SURREAL0

deffunc H₁( Sequence) -> set = bool (union (rng $1));
deffunc H₂( Sequence) -> set = [:H₁($1),H₁($1):];
consider L being Sequence such that
A1: dom L = succ A and
A2: for B being Ordinal
for L1 being Sequence st B in succ A & L1 = L | B holds
L . B = H₂(L1) from ORDINAL1:sch 4();
thus ex IT being set ex L being Sequence st
( IT = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:H₁(L | O),H₁(L | O):] ) ) :: thesis:

take IT = L . A; :: thesis:
take L ; :: thesis:
thus ( IT = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:H₁(L | O),H₁(L | O):] ) ) by A1, A2; :: thesis:

end;

let it1, it2 be set ; :: thesis:
given L1 being Sequence such that A3: ( it1 = L1 . A & dom L1 = succ A & ( for O being Ordinal st O in succ A holds
L1 . O = [:H₁(L1 | O),H₁(L1 | O):] ) ) ; :: thesis:
given L2 being Sequence such that A4: ( it2 = L2 . A & dom L2 = succ A & ( for O being Ordinal st O in succ A holds
L2 . O = [:H₁(L2 | O),H₁(L2 | O):] ) ) ; :: thesis:
A5: ( dom L1 = succ A & ( for B being Ordinal
for L being Sequence st B in succ A & L = L1 | B holds
L1 . B = H₂(L) ) ) by A3;
A6: ( dom L2 = succ A & ( for B being Ordinal
for L being Sequence st B in succ A & L = L2 | B holds
L2 . B = H₂(L) ) ) by A4;
L1 = L2 from ORDINAL1:sch 3(A5, A6);
hence it1 = it2 by A3, A4; :: thesis:

end;

:: deftheorem Def4 defines Games SURREAL0:def 4 :

registration

let A be Ordinal;

cluster Games A -> non empty Relation-like ;

consider L being Sequence such that
A1: ( Games A = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] ) ) by Def4;
L . A = [:(bool (union (rng (L | A)))),(bool (union (rng (L | A)))):] by A1, ORDINAL1:6;
hence ( not Games A is empty & Games A is Relation-like ) by A1; :: thesis:

end;

theorem Th1: :: SURREAL0:1

for A, B being Ordinal st A c= B holds
Games A c= Games B

let A, B be Ordinal; :: thesis:
assume A1: A c= B ; :: thesis:
consider La being Sequence such that
A2: ( Games A = La . A & dom La = succ A & ( for O being Ordinal st O in succ A holds
La . O = [:(bool (union (rng (La | O)))),(bool (union (rng (La | O)))):] ) ) by Def4;
consider Lb being Sequence such that
A3: ( Games B = Lb . B & dom Lb = succ B & ( for O being Ordinal st O in succ B holds
Lb . O = [:(bool (union (rng (Lb | O)))),(bool (union (rng (Lb | O)))):] ) ) by Def4;
defpred S₁[ Ordinal] means ( $1 c= A implies La . $1 = Lb . $1 );
A4: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

let D be Ordinal; :: thesis:
assume A5: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:
assume A6: D c= A ; :: thesis:
B c= succ B by XBOOLE_1:7;
then ( A c= succ A & A c= succ B ) by XBOOLE_1:7, A1, XBOOLE_1:1;
then A7: ( dom (La | D) = D & D = dom (Lb | D) ) by A2, A3, RELAT_1:62, A6, XBOOLE_1:1;
for x being object st x in D holds
(La | D) . x = (Lb | D) . x

let x be object ; :: thesis:
assume A8: x in D ; :: thesis:
reconsider o = x as Ordinal by A8;
thus (La | D) . x = La . o by A8, FUNCT_1:49
.= Lb . o by A8, ORDINAL1:def 2, A6, A5
.= (Lb | D) . x by A8, FUNCT_1:49 ; :: thesis:

end;

then A9: La | D = Lb | D by A7, FUNCT_1:2;
A10: ( D c= B & B in succ B ) by A1, A6, ORDINAL1:6, XBOOLE_1:1;
D in succ A by ORDINAL1:6, A6, ORDINAL1:12;
hence La . D = [:(bool (union (rng (Lb | D)))),(bool (union (rng (Lb | D)))):] by A2, A9
.= Lb . D by A10, A3, ORDINAL1:12 ;
:: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A14: y in rng (La | A) ; :: thesis:
consider x being object such that
A15: ( x in dom (La | A) & (La | A) . x = y ) by A14, FUNCT_1:def 3;
A16: ( dom (La | A) = A & dom (Lb | B) = B ) by A2, A3, RELAT_1:62, XBOOLE_1:7;
reconsider x = x as Ordinal by A15;
(La | A) . x = La . x by A15, FUNCT_1:49
.= Lb . x by A15, ORDINAL1:def 2, A11
.= (Lb | B) . x by A1, A15, A16, FUNCT_1:49 ;
hence y in rng (Lb | B) by A1, A16, A15, FUNCT_1:def 3; :: thesis:

end;

then union (rng (La | A)) c= union (rng (Lb | B)) by ZFMISC_1:77;
then bool (union (rng (La | A))) c= bool (union (rng (Lb | B))) by ZFMISC_1:67;
hence Games A c= Games B by A2, A3, A12, A13, ZFMISC_1:96; :: thesis:

end;

theorem Th2: :: SURREAL0:2

Games 0 = {[{},{}]}

consider L being Sequence such that
A1: ( Games 0 = L . 0 & dom L = succ 0 ) and
A2: for O being Ordinal st O in succ 0 holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] by Def4;
A3: L . 0 = [:(bool (union (rng (L | 0)))),(bool (union (rng (L | 0)))):] by A2, ORDINAL1:6;
bool (union (rng (L | 0))) = {{}} by ZFMISC_1:1, ZFMISC_1:2;
hence Games 0 = {[{},{}]} by A1, A3, ZFMISC_1:29; :: thesis:

end;

theorem Th3: :: SURREAL0:3

for L being Sequence
for O being Ordinal st dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = [:(bool (union (rng (L | A)))),(bool (union (rng (L | A)))):] ) holds
for A being Ordinal st A in succ O holds
L . A = Games A

let L be Sequence; :: thesis:
let Ord be Ordinal; :: thesis:
assume that
A1: dom L = succ Ord and
A2: for A being Ordinal st A in succ Ord holds
L . A = [:(bool (union (rng (L | A)))),(bool (union (rng (L | A)))):] ; :: thesis:
let O be Ordinal; :: thesis:
assume A3: O in succ Ord ; :: thesis:
consider LO being Sequence such that
A4: ( Games O = LO . O & dom LO = succ O ) and
A5: for A being Ordinal st A in succ O holds
LO . A = [:(bool (union (rng (LO | A)))),(bool (union (rng (LO | A)))):] by Def4;
defpred S₁[ Ordinal] means ( $1 c= O implies LO . $1 = L . $1 );
A6: for A being Ordinal st ( for C being Ordinal st C in A holds
S₁[C] ) holds
S₁[A]

let A be Ordinal; :: thesis:
assume A7: for C being Ordinal st C in A holds
S₁[C] ; :: thesis:
assume A8: A c= O ; :: thesis:
then A9: A in succ O by ORDINAL1:22;
A10: A in succ Ord by A8, A3, ORDINAL1:12;
A11: L . A = [:(bool (union (rng (L | A)))),(bool (union (rng (L | A)))):] by A2, A8, A3, ORDINAL1:12;
A12: ( dom (L | A) = A & dom (LO | A) = A ) by A4, A1, A9, ORDINAL1:def 2, RELAT_1:62, A10;
for x being object st x in A holds
(LO | A) . x = (L | A) . x

let x be object ; :: thesis:
assume A13: x in A ; :: thesis:
reconsider x = x as Ordinal by A13;
(LO | A) . x = LO . x by A13, FUNCT_1:49
.= L . x by A13, A7, A8, ORDINAL1:def 2 ;
hence (LO | A) . x = (L | A) . x by A13, FUNCT_1:49; :: thesis:

end;

then LO | A = L | A by A12, FUNCT_1:2;
hence LO . A = L . A by A5, A8, ORDINAL1:22, A11; :: thesis:

end;

for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A6);
hence L . O = Games O by A4; :: thesis:

end;

theorem Th4: :: SURREAL0:4

for O being Ordinal
for o being object holds
( o in Games O iff ( o is pair & ( for a being object st a in (L_ o) \/ (R_ o) holds
ex A being Ordinal st
( A in O & a in Games A ) ) ) )

let O be Ordinal; :: thesis:
let o be object ; :: thesis:
consider L being Sequence such that
A1: ( Games O = L . O & dom L = succ O ) and
A2: for A being Ordinal st A in succ O holds
L . A = [:(bool (union (rng (L | A)))),(bool (union (rng (L | A)))):] by Def4;
A3: O in succ O by ORDINAL1:6;
A4: Games O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] by A1, A2, ORDINAL1:6;
A5: dom (L | O) = O by RELAT_1:62, A1, A3, ORDINAL1:def 2;
thus ( o in Games O implies ( o is pair & ( for x being object st x in (L_ o) \/ (R_ o) holds
ex B being Ordinal st
( B in O & x in Games B ) ) ) ) :: thesis:

assume o in Games O ; :: thesis:
then consider x, y being object such that
A6: ( x in bool (union (rng (L | O))) & y in bool (union (rng (L | O))) & o = [x,y] ) by A4, ZFMISC_1:def 2;
reconsider x = x, y = y as set by TARSKI:1;
thus o is pair by A6; :: thesis:
let z be object ; :: thesis:
assume A7: z in (L_ o) \/ (R_ o) ; :: thesis:
x \/ y c= union (rng (L | O)) by A6, XBOOLE_1:8;
then consider Y being set such that
A8: ( z in Y & Y in rng (L | O) ) by A6, A7, TARSKI:def 4;
consider OO being object such that
A9: ( OO in dom (L | O) & (L | O) . OO = Y ) by A8, FUNCT_1:def 3;
reconsider OO = OO as Ordinal by A9;
take OO ; :: thesis:
A10: OO in succ O by ORDINAL1:8, A9;
(L | O) . OO = L . OO by A9, FUNCT_1:49;
hence ( OO in O & z in Games OO ) by A9, A1, A8, A10, A2, Th3; :: thesis:

end;

assume that
A11: o is pair and
A12: for x being object st x in (L_ o) \/ (R_ o) holds
ex B being Ordinal st
( B in O & x in Games B ) ; :: thesis:
A13: (L_ o) \/ (R_ o) c= union (rng (L | O))

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A14: x in (L_ o) \/ (R_ o) ; :: thesis:
consider B being Ordinal such that
A15: ( B in O & x in Games B ) by A14, A12;
B in succ O by A15, ORDINAL1:8;
then ( Games B = L . B & L . B = (L | O) . B & (L | O) . B in rng (L | O) ) by A5, A15, A1, A2, Th3, FUNCT_1:49, FUNCT_1:def 3;
hence x in union (rng (L | O)) by A15, TARSKI:def 4; :: thesis:

end;

( L_ o c= (L_ o) \/ (R_ o) & R_ o c= (L_ o) \/ (R_ o) ) by XBOOLE_1:7;
then ( L_ o c= union (rng (L | O)) & R_ o c= union (rng (L | O)) ) by A13, XBOOLE_1:1;
hence o in Games O by A11, A4, ZFMISC_1:def 2; :: thesis:

end;

definition

let A be Ordinal;

func BeforeGames A -> Subset of (Games A) means :Def5: :: SURREAL0:def 5
for a being object holds
( a in it iff ex O being Ordinal st
( O in A & a in Games O ) );

defpred S₁[ object ] means ex O being Ordinal st
( O in A & $1 in Games O );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in Games A & S₁[x] ) ) from XBOOLE_0:sch 1();
X c= Games A

let x be object ; :: according to TARSKI:def 3 :: thesis:
thus ( not x in X or x in Games A ) by A1; :: thesis:

end;

then reconsider X = X as Subset of (Games A) ;
take X ; :: thesis:
let x be object ; :: thesis:
thus ( x in X implies ex O being Ordinal st
( O in A & x in Games O ) ) by A1; :: thesis:
given O being Ordinal such that A2: ( O in A & x in Games O ) ; :: thesis:
Games O c= Games A by A2, Th1, ORDINAL1:def 2;
hence x in X by A2, A1; :: thesis:

end;

let B1, B2 be Subset of (Games A); :: thesis:
assume that
A3: for x being object holds
( x in B1 iff ex O being Ordinal st
( O in A & x in Games O ) ) and
A4: for x being object holds
( x in B2 iff ex O being Ordinal st
( O in A & x in Games O ) ) ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
( x in B1 iff ex O being Ordinal st
( O in A & x in Games O ) ) by A3;
hence ( x in B1 iff x in B2 ) by A4; :: thesis:

end;

hence B1 = B2 by TARSKI:2; :: thesis:

end;

:: deftheorem Def5 defines BeforeGames SURREAL0:def 5 :

theorem Th5: :: SURREAL0:5

for A, B being Ordinal st A c= B holds
BeforeGames A c= BeforeGames B

let A, B be Ordinal; :: thesis:
assume A1: A c= B ; :: thesis:
let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume [x,y] in BeforeGames A ; :: thesis:
then ex O being Ordinal st
( O in A & [x,y] in Games O ) by Def5;
hence [x,y] in BeforeGames B by A1, Def5; :: thesis:

end;

definition

let O be Ordinal;
let R be Relation;

func Day (R,O) -> Subset of (Games O) means :Def6: :: SURREAL0:def 6
ex L being Sequence st
( it = L . O & dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ) );

deffunc H₁( Sequence) -> set = { x where x is Element of Games (dom $1) : ( L_ x c= union (rng $1) & R_ x c= union (rng $1) & L_ x << R, R_ x ) } ;
consider L being Sequence such that
A1: dom L = succ O and
A2: for B being Ordinal
for L1 being Sequence st B in succ O & L1 = L | B holds
L . B = H₁(L1) from ORDINAL1:sch 4();
A3: O in succ O by ORDINAL1:6;
A4: L . O = H₁(L | O) by A2, ORDINAL1:6;
A5: dom (L | O) = O by RELAT_1:62, A3, A1, ORDINAL1:def 2;
L . O c= Games O

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in L . O ; :: thesis:
then ex x being Element of Games O st
( y = x & L_ x c= union (rng (L | O)) & R_ x c= union (rng (L | O)) & L_ x << R, R_ x ) by A4, A5;
hence y in Games O ; :: thesis:

end;

then reconsider IT = L . O as Subset of (Games O) ;
take IT ; :: thesis:
take L ; :: thesis:
thus ( IT = L . O & dom L = succ O ) by A1; :: thesis:
let A be Ordinal; :: thesis:
assume A6: A in succ O ; :: thesis:
A7: dom (L | A) = A by A1, RELAT_1:62, A6, ORDINAL1:def 2;
hence L . A c= { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } by A2, A6; :: according to XBOOLE_0:def 10 :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ; :: thesis:
hence y in L . A by A7, A2, A6; :: thesis:

end;

let X1, X2 be Subset of (Games O); :: thesis:
given L1 being Sequence such that A8: ( X1 = L1 . O & dom L1 = succ O ) and
A9: for A being Ordinal st A in succ O holds
L1 . A = { x where x is Element of Games A : ( L_ x c= union (rng (L1 | A)) & R_ x c= union (rng (L1 | A)) & L_ x << R, R_ x ) } ; :: thesis:
given L2 being Sequence such that A10: ( X2 = L2 . O & dom L2 = succ O ) and
A11: for A being Ordinal st A in succ O holds
L2 . A = { x where x is Element of Games A : ( L_ x c= union (rng (L2 | A)) & R_ x c= union (rng (L2 | A)) & L_ x << R, R_ x ) } ; :: thesis:
deffunc H₁( Sequence) -> set = { x where x is Element of Games (dom $1) : ( L_ x c= union (rng $1) & R_ x c= union (rng $1) & L_ x << R, R_ x ) } ;
A12: ( dom L1 = succ O & ( for B being Ordinal
for L being Sequence st B in succ O & L = L1 | B holds
L1 . B = H₁(L) ) )

thus dom L1 = succ O by A8; :: thesis:
let B be Ordinal; :: thesis:
let L be Sequence; :: thesis:
assume A13: ( B in succ O & L = L1 | B ) ; :: thesis:
A14: dom (L1 | B) = B by A13, A8, RELAT_1:62, ORDINAL1:def 2;
thus L1 . B c= H₁(L) by A14, A13, A9; :: according to XBOOLE_0:def 10 :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
thus ( not y in H₁(L) or y in L1 . B ) by A13, A14, A9; :: thesis:

end;

A15: ( dom L2 = succ O & ( for B being Ordinal
for L being Sequence st B in succ O & L = L2 | B holds
L2 . B = H₁(L) ) )

thus dom L2 = succ O by A10; :: thesis:
let B be Ordinal; :: thesis:
let L be Sequence; :: thesis:
assume A16: ( B in succ O & L = L2 | B ) ; :: thesis:
dom (L2 | B) = B by A16, A10, RELAT_1:62, ORDINAL1:def 2;
hence L2 . B = H₁(L) by A16, A11; :: thesis:

end;

L1 = L2 from ORDINAL1:sch 3(A12, A15);
hence X1 = X2 by A8, A10; :: thesis:

end;

:: deftheorem Def6 defines Day SURREAL0:def 6 :

definition

let R be Relation;

attr R is almost-No-order means :: SURREAL0:def 7
ex O being Ordinal st R c= [:(Day (R,O)),(Day (R,O)):];

end;

:: deftheorem defines almost-No-order SURREAL0:def 7 :

theorem Th6: :: SURREAL0:6

for O being Ordinal
for R being Relation
for L being Sequence st dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ) holds
for A being Ordinal st A in succ O holds
L . A = Day (R,A)

let O be Ordinal; :: thesis:
let R be Relation; :: thesis:
let L be Sequence; :: thesis:
assume that
A1: dom L = succ O and
A2: for A being Ordinal st A in succ O holds
L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ; :: thesis:
let D be Ordinal; :: thesis:
assume A3: D in succ O ; :: thesis:
consider LO being Sequence such that
A4: ( Day (R,D) = LO . D & dom LO = succ D ) and
A5: for A being Ordinal st A in succ D holds
LO . A = { x where x is Element of Games A : ( L_ x c= union (rng (LO | A)) & R_ x c= union (rng (LO | A)) & L_ x << R, R_ x ) } by Def6;
defpred S₁[ Ordinal] means ( $1 c= D implies LO . $1 = L . $1 );
A6: for A being Ordinal st ( for C being Ordinal st C in A holds
S₁[C] ) holds
S₁[A]

let A be Ordinal; :: thesis:
assume A7: for C being Ordinal st C in A holds
S₁[C] ; :: thesis:
assume A8: A c= D ; :: thesis:
then A9: A in succ D by ORDINAL1:22;
A10: A in succ O by A8, A3, ORDINAL1:12;
A11: L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } by A2, A8, A3, ORDINAL1:12;
A12: ( dom (L | A) = A & dom (LO | A) = A ) by A4, A1, A9, ORDINAL1:def 2, RELAT_1:62, A10;
for x being object st x in A holds
(LO | A) . x = (L | A) . x

end;

then LO | A = L | A by A12, FUNCT_1:2;
hence LO . A = L . A by A8, ORDINAL1:22, A5, A11; :: thesis:

end;

for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A6);
hence L . D = Day (R,D) by A4; :: thesis:

end;

theorem Th7: :: SURREAL0:7

for O being Ordinal
for R being Relation
for x being Element of Games O holds
( x in Day (R,O) iff ( L_ x << R, R_ x & ( for o being object st o in (L_ x) \/ (R_ x) holds
ex A being Ordinal st
( A in O & o in Day (R,A) ) ) ) )

let O be Ordinal; :: thesis:
let R be Relation; :: thesis:
let A be Element of Games O; :: thesis:
consider L being Sequence such that
A1: ( Day (R,O) = L . O & dom L = succ O ) and
A2: for A being Ordinal st A in succ O holds
L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } by Def6;
A3: O in succ O by ORDINAL1:6;
A4: Day (R,O) = { x where x is Element of Games O : ( L_ x c= union (rng (L | O)) & R_ x c= union (rng (L | O)) & L_ x << R, R_ x ) } by A1, A2, ORDINAL1:6;
A5: dom (L | O) = O by RELAT_1:62, A1, A3, ORDINAL1:def 2;
thus ( A in Day (R,O) implies ( L_ A << R, R_ A & ( for x being object st x in (L_ A) \/ (R_ A) holds
ex B being Ordinal st
( B in O & x in Day (R,B) ) ) ) ) :: thesis:

assume A in Day (R,O) ; :: thesis:
then consider x being Element of Games O such that
A6: ( A = x & L_ x c= union (rng (L | O)) & R_ x c= union (rng (L | O)) & L_ x << R, R_ x ) by A4;
thus L_ A << R, R_ A by A6; :: thesis:
let y be object ; :: thesis:
assume A7: y in (L_ A) \/ (R_ A) ; :: thesis:
(L_ x) \/ (R_ x) c= union (rng (L | O)) by A6, XBOOLE_1:8;
then consider Y being set such that
A8: ( y in Y & Y in rng (L | O) ) by A6, A7, TARSKI:def 4;
consider B being object such that
A9: ( B in dom (L | O) & (L | O) . B = Y ) by A8, FUNCT_1:def 3;
reconsider B = B as Ordinal by A9;
take B ; :: thesis:
A10: B in succ O by A9, ORDINAL1:8;
(L | O) . B = L . B by A9, FUNCT_1:49;
hence ( B in O & y in Day (R,B) ) by A9, A1, A8, A10, A2, Th6; :: thesis:

end;

assume that
A11: L_ A << R, R_ A and
A12: for x being object st x in (L_ A) \/ (R_ A) holds
ex B being Ordinal st
( B in O & x in Day (R,B) ) ; :: thesis:
A13: (L_ A) \/ (R_ A) c= union (rng (L | O))

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A14: x in (L_ A) \/ (R_ A) ; :: thesis:
consider B being Ordinal such that
A15: ( B in O & x in Day (R,B) ) by A14, A12;
B in succ O by A15, ORDINAL1:8;
then ( Day (R,B) = L . B & L . B = (L | O) . B & (L | O) . B in rng (L | O) ) by A5, A15, A1, A2, Th6, FUNCT_1:49, FUNCT_1:def 3;
hence x in union (rng (L | O)) by A15, TARSKI:def 4; :: thesis:

end;

( L_ A c= (L_ A) \/ (R_ A) & R_ A c= (L_ A) \/ (R_ A) ) by XBOOLE_1:7;
then ( L_ A c= union (rng (L | O)) & R_ A c= union (rng (L | O)) ) by A13, XBOOLE_1:1;
hence A in Day (R,O) by A11, A4; :: thesis:

end;

theorem Th8: :: SURREAL0:8

for R being Relation holds Day (R,0) = Games 0

let R be Relation; :: thesis:
reconsider A = [{},{}] as Element of Games 0 by Th2, TARSKI:def 1;
A1: L_ A << R, R_ A ;
for x being object st x in (L_ A) \/ (R_ A) holds
ex O being Ordinal st
( O in 0 & x in Day (R,O) ) ;
then A in Day (R,0) by Th7, A1;
hence Day (R,0) = Games 0 by Th2, ZFMISC_1:33; :: thesis:

end;

theorem Th9: :: SURREAL0:9

for A, B being Ordinal
for R being Relation st A c= B holds
Day (R,A) c= Day (R,B)

let A, B be Ordinal; :: thesis:
let R be Relation; :: thesis:
assume A1: A c= B ; :: thesis:
let x1, x2 be object ; :: according to RELAT_1:def 3 :: thesis:
set x = [x1,x2];
assume A2: [x1,x2] in Day (R,A) ; :: thesis:
then A3: [x1,x2] in Games A ;
A4: ( L_ [x1,x2] << R, R_ [x1,x2] & ( for y being object st y in (L_ [x1,x2]) \/ (R_ [x1,x2]) holds
ex O being Ordinal st
( O in A & y in Day (R,O) ) ) ) by Th7, A2;
A5: Games A c= Games B by A1, Th1;
for y being object st y in (L_ [x1,x2]) \/ (R_ [x1,x2]) holds
ex O being Ordinal st
( O in B & y in Day (R,O) )

let y be object ; :: thesis:
assume y in (L_ [x1,x2]) \/ (R_ [x1,x2]) ; :: thesis:
then ex O being Ordinal st
( O in A & y in Day (R,O) ) by Th7, A2;
hence ex O being Ordinal st
( O in B & y in Day (R,O) ) by A1; :: thesis:

end;

hence [x1,x2] in Day (R,B) by A4, A5, A3, Th7; :: thesis:

end;

registration

let R be Relation;
let A be Ordinal;

cluster Day (R,A) -> non empty ;

{} c= A ;
then Day (R,{}) c= Day (R,A) by Th9;
hence not Day (R,A) is empty by Th8; :: thesis:

end;

Lm1: for A being Ordinal
for R, S being Relation st R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
Day (R,A) = Day (S,A)

let A be Ordinal; :: thesis:
defpred S₁[ Ordinal] means for R, S being Relation st R /\ [:(BeforeGames $1),(BeforeGames $1):] = S /\ [:(BeforeGames $1),(BeforeGames $1):] holds
Day (R,$1) c= Day (S,$1);
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

let D be Ordinal; :: thesis:
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:
let R, S be Relation; :: thesis:
assume A3: R /\ [:(BeforeGames D),(BeforeGames D):] = S /\ [:(BeforeGames D),(BeforeGames D):] ; :: thesis:
let x1, x2 be object ; :: according to RELAT_1:def 3 :: thesis:
assume A4: [x1,x2] in Day (R,D) ; :: thesis:
set x = [x1,x2];
reconsider A = [x1,x2] as Element of Games D by A4;
A5: ( L_ A << R, R_ A & ( for x being object st x in (L_ A) \/ (R_ A) holds
ex O being Ordinal st
( O in D & x in Day (R,O) ) ) ) by A4, Th7;
A6: L_ A << S, R_ A

let l, r be object ; :: according to SURREAL0:def 3 :: thesis:
assume A7: ( l in L_ A & r in R_ A ) ; :: thesis:
l in (L_ A) \/ (R_ A) by A7, XBOOLE_0:def 3;
then consider OL being Ordinal such that
A8: ( OL in D & l in Day (R,OL) ) by A4, Th7;
r in (L_ A) \/ (R_ A) by A7, XBOOLE_0:def 3;
then consider OR being Ordinal such that
A9: ( OR in D & r in Day (R,OR) ) by A4, Th7;
( l in BeforeGames D & r in BeforeGames D ) by A8, A9, Def5;
then A10: [r,l] in [:(BeforeGames D),(BeforeGames D):] by ZFMISC_1:87;
A11: not l >= R,r by A7, A5;
assume l >= S,r ; :: thesis:
then [r,l] in R /\ [:(BeforeGames D),(BeforeGames D):] by A10, A3, XBOOLE_0:def 4;
hence contradiction by A11, XBOOLE_0:def 4; :: thesis:

end;

for x being object st x in (L_ A) \/ (R_ A) holds
ex O being Ordinal st
( O in D & x in Day (S,O) )

let x be object ; :: thesis:
assume A12: x in (L_ A) \/ (R_ A) ; :: thesis:
consider O being Ordinal such that
A13: ( O in D & x in Day (R,O) ) by A12, A4, Th7;
BeforeGames O c= BeforeGames D by Th5, A13, ORDINAL1:def 2;
then A14: [:(BeforeGames O),(BeforeGames O):] /\ [:(BeforeGames D),(BeforeGames D):] = [:(BeforeGames O),(BeforeGames O):] by XBOOLE_1:28, ZFMISC_1:96;
then A15: R /\ [:(BeforeGames O),(BeforeGames O):] = (S /\ [:(BeforeGames D),(BeforeGames D):]) /\ [:(BeforeGames O),(BeforeGames O):] by A3, XBOOLE_1:16
.= S /\ [:(BeforeGames O),(BeforeGames O):] by A14, XBOOLE_1:16 ;
Day (R,O) c= Day (S,O) by A15, A13, A2;
hence ex O being Ordinal st
( O in D & x in Day (S,O) ) by A13; :: thesis:

end;

hence [x1,x2] in Day (S,D) by A6, Th7; :: thesis:

end;

A16: for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
let R, S be Relation; :: thesis:
assume A17: R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis:
( Day (R,A) c= Day (S,A) & Day (S,A) c= Day (R,A) ) by A16, A17;
hence Day (R,A) = Day (S,A) by XBOOLE_0:def 10; :: thesis:

end;

theorem Th10: :: SURREAL0:10

for A, B being Ordinal
for R, S being Relation st B c= A & R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
Day (R,B) = Day (S,B)

let A, B be Ordinal; :: thesis:
let R, S be Relation; :: thesis:
assume that
A1: B c= A and
A2: R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis:
BeforeGames B c= BeforeGames A by A1, Th5;
then A3: [:(BeforeGames B),(BeforeGames B):] /\ [:(BeforeGames A),(BeforeGames A):] = [:(BeforeGames B),(BeforeGames B):] by XBOOLE_1:28, ZFMISC_1:96;
then R /\ [:(BeforeGames B),(BeforeGames B):] = (S /\ [:(BeforeGames A),(BeforeGames A):]) /\ [:(BeforeGames B),(BeforeGames B):] by A2, XBOOLE_1:16
.= S /\ [:(BeforeGames B),(BeforeGames B):] by A3, XBOOLE_1:16 ;
hence Day (R,B) = Day (S,B) by Lm1; :: thesis:

end;

definition

let R be Relation;
let o be object ;
assume A1: ex O being Ordinal st o in Day (R,O) ;

func born (R,o) -> Ordinal means :Def8: :: SURREAL0:def 8
( o in Day (R,it) & ( for O being Ordinal st o in Day (R,O) holds
it c= O ) );

defpred S₁[ Ordinal] means o in Day (R,$1);
A2: ex O being Ordinal st S₁[O] by A1;
ex A being Ordinal st
( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A2);
hence ex b₁ being Ordinal st
( o in Day (R,b₁) & ( for O being Ordinal st o in Day (R,O) holds
b₁ c= O ) ) ; :: thesis:

end;

let it1, it2 be Ordinal; :: thesis:
assume that
A3: ( o in Day (R,it1) & ( for O being Ordinal st o in Day (R,O) holds
it1 c= O ) ) and
A4: ( o in Day (R,it2) & ( for O being Ordinal st o in Day (R,O) holds
it2 c= O ) ) ; :: thesis:
( it1 c= it2 & it2 c= it1 ) by A3, A4;
hence it1 = it2 by XBOOLE_0:def 10; :: thesis:

end;

:: deftheorem Def8 defines born SURREAL0:def 8 :

theorem Th11: :: SURREAL0:11

for A being Ordinal
for R, S being Relation st R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
for a being object st a in Day (R,A) holds
born (R,a) = born (S,a)

let A be Ordinal; :: thesis:
let R, S be Relation; :: thesis:
assume A1: R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis:
A2: Day (R,A) = Day (S,A) by A1, Th10;
let x be object ; :: thesis:
assume A3: x in Day (R,A) ; :: thesis:
A4: x in Day (S,A) by A3, A1, Th10;
born (R,x) c= A by A3, Def8;
then Day (R,(born (R,x))) = Day (S,(born (R,x))) by A1, Th10;
then x in Day (S,(born (R,x))) by A3, Def8;
then A5: born (S,x) c= born (R,x) by Def8;
born (S,x) c= A by A3, A2, Def8;
then Day (S,(born (S,x))) = Day (R,(born (S,x))) by A1, Th10;
then x in Day (R,(born (S,x))) by A4, Def8;
then born (R,x) c= born (S,x) by Def8;
hence born (R,x) = born (S,x) by A5, XBOOLE_0:def 10; :: thesis:

end;

theorem Th12: :: SURREAL0:12

for A, O being Ordinal
for R being Relation
for o being object st o in Games O & not o in Day (R,O) holds
not o in Day (R,A)

let A, O be Ordinal; :: thesis:
let R be Relation; :: thesis:
let o be object ; :: thesis:
defpred S₁[ Ordinal] means for x being object
for O being Ordinal st x in (Games O) \ (Day (R,O)) holds
not x in Day (R,$1);
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

let D be Ordinal; :: thesis:
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:
let x be object ; :: thesis:
let O be Ordinal; :: thesis:
assume that
A3: x in (Games O) \ (Day (R,O)) and
A4: x in Day (R,D) ; :: thesis:
reconsider xD = x as Element of Games D by A4;
reconsider xO = x as Element of Games O by A3;
A5: ( L_ xD << R, R_ xD & ( for x being object st x in (L_ xD) \/ (R_ xD) holds
ex O being Ordinal st
( O in D & x in Day (R,O) ) ) ) by A4, Th7;
not xO in Day (R,O) by A3, XBOOLE_0:def 5;
then consider y being object such that
A6: ( y in (L_ xO) \/ (R_ xO) & ( for H being Ordinal st H in O holds
not y in Day (R,H) ) ) by A5, Th7;
consider H being Ordinal such that
A7: ( H in O & y in Games H ) by A6, Th4;
not y in Day (R,H) by A6, A7;
then A8: y in (Games H) \ (Day (R,H)) by A7, XBOOLE_0:def 5;
ex W being Ordinal st
( W in D & y in Day (R,W) ) by A6, A4, Th7;
hence contradiction by A8, A2; :: thesis:

end;

A9: for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
assume ( o in Games O & not o in Day (R,O) ) ; :: thesis:
then o in (Games O) \ (Day (R,O)) by XBOOLE_0:def 5;
hence not o in Day (R,A) by A9; :: thesis:

end;

definition

let R be Relation;
let A, B be Ordinal;

func OpenProd (R,A,B) -> Relation of (Day (R,A)) means :Def9: :: SURREAL0:def 9
for x, y being Element of Day (R,A) holds
( [x,y] in it iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) );

defpred S₁[ object , object ] means ( ( born (R,$1) in A & born (R,$2) in A ) or ( born (R,$1) = A & born (R,$2) in B ) or ( born (R,$1) in B & born (R,$2) = A ) );
ex I being Relation of (Day (R,A)),(Day (R,A)) st
for x, y being Element of Day (R,A) holds
( [x,y] in I iff S₁[x,y] ) from RELSET_1:sch 2();
hence ex b₁ being Relation of (Day (R,A)) st
for x, y being Element of Day (R,A) holds
( [x,y] in b₁ iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) ) ; :: thesis:

end;

defpred S₁[ object , object ] means ( ( born (R,$1) in A & born (R,$2) in A ) or ( born (R,$1) = A & born (R,$2) in B ) or ( born (R,$1) in B & born (R,$2) = A ) );
let I1, I2 be Relation of (Day (R,A)); :: thesis:
assume that
A1: for x, y being Element of Day (R,A) holds
( [x,y] in I1 iff S₁[x,y] ) and
A2: for x, y being Element of Day (R,A) holds
( [x,y] in I2 iff S₁[x,y] ) ; :: thesis:
I1 = I2 from RELSET_1:sch 4(A1, A2);
hence I1 = I2 ; :: thesis:

end;

:: deftheorem Def9 defines OpenProd SURREAL0:def 9 :

definition

let R be Relation;
let A, B be Ordinal;

func ClosedProd (R,A,B) -> Relation of (Day (R,A)) means :Def10: :: SURREAL0:def 10
for x, y being Element of Day (R,A) holds
( [x,y] in it iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) );

defpred S₁[ object , object ] means ( ( born (R,$1) in A & born (R,$2) in A ) or ( born (R,$1) = A & born (R,$2) c= B ) or ( born (R,$1) c= B & born (R,$2) = A ) );
ex I being Relation of (Day (R,A)),(Day (R,A)) st
for x, y being Element of Day (R,A) holds
( [x,y] in I iff S₁[x,y] ) from RELSET_1:sch 2();
hence ex b₁ being Relation of (Day (R,A)) st
for x, y being Element of Day (R,A) holds
( [x,y] in b₁ iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) ) ; :: thesis:

end;

defpred S₁[ object , object ] means ( ( born (R,$1) in A & born (R,$2) in A ) or ( born (R,$1) = A & born (R,$2) c= B ) or ( born (R,$1) c= B & born (R,$2) = A ) );
let I1, I2 be Relation of (Day (R,A)); :: thesis:
assume that
A1: for x, y being Element of Day (R,A) holds
( [x,y] in I1 iff S₁[x,y] ) and
A2: for x, y being Element of Day (R,A) holds
( [x,y] in I2 iff S₁[x,y] ) ; :: thesis:
I1 = I2 from RELSET_1:sch 4(A1, A2);
hence I1 = I2 ; :: thesis:

end;

:: deftheorem Def10 defines ClosedProd SURREAL0:def 10 :

theorem :: SURREAL0:13

for A1, A2, B1, B2 being Ordinal
for R being Relation st ( A1 in A2 or ( A1 = A2 & B1 c= B2 ) ) holds
OpenProd (R,A1,B1) c= OpenProd (R,A2,B2)

let A1, A2, B1, B2 be Ordinal; :: thesis:
let R be Relation; :: thesis:
assume A1: ( A1 in A2 or ( A1 = A2 & B1 c= B2 ) ) ; :: thesis:
A2: A1 c= A2 by A1, ORDINAL1:def 2;
A3: Day (R,A1) c= Day (R,A2) by A1, ORDINAL1:def 2, Th9;
let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A4: [x,y] in OpenProd (R,A1,B1) ; :: thesis:
A5: ( x in Day (R,A1) & y in Day (R,A1) ) by A4, ZFMISC_1:87;

per cases by A5, A4, Def9;

suppose ( born (R,x) in A1 & born (R,y) in A1 ) ; :: thesis:

hence [x,y] in OpenProd (R,A2,B2) by A2, A3, A5, Def9; :: thesis:

end;

suppose A6: ( born (R,x) = A1 & born (R,y) in B1 ) ; :: thesis:

per cases by A1;

suppose A7: A1 in A2 ; :: thesis:

born (R,y) c= A1 by A5, Def8;
then born (R,y) in A2 by A7, ORDINAL1:12;
hence [x,y] in OpenProd (R,A2,B2) by A6, A7, A5, A3, Def9; :: thesis:

end;

suppose ( A1 = A2 & B1 c= B2 ) ; :: thesis:

hence [x,y] in OpenProd (R,A2,B2) by A6, A5, Def9; :: thesis:

end;

suppose A8: ( born (R,x) in B1 & born (R,y) = A1 ) ; :: thesis:

per cases by A1;

suppose A9: A1 in A2 ; :: thesis:

born (R,x) c= A1 by A5, Def8;
then born (R,x) in A2 by A9, ORDINAL1:12;
hence [x,y] in OpenProd (R,A2,B2) by A8, A9, A5, A3, Def9; :: thesis:

end;

suppose ( A1 = A2 & B1 c= B2 ) ; :: thesis:

hence [x,y] in OpenProd (R,A2,B2) by A8, A5, Def9; :: thesis:

end;

theorem :: SURREAL0:14

for A, B being Ordinal
for R, S being Relation st R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
OpenProd (R,A,B) = OpenProd (S,A,B)

let A, B be Ordinal; :: thesis:
let R, S be Relation; :: thesis:
assume A1: R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis:
A2: Day (R,A) = Day (S,A) by A1, Th10;
let x, y be object ; :: according to RELAT_1:def 2 :: thesis:
thus ( [x,y] in OpenProd (R,A,B) implies [x,y] in OpenProd (S,A,B) ) :: thesis:

assume A3: [x,y] in OpenProd (R,A,B) ; :: thesis:
A4: ( x in Day (R,A) & y in Day (R,A) ) by A3, ZFMISC_1:87;
A5: ( born (R,x) = born (S,x) & born (R,y) = born (S,y) ) by A1, A4, Th11;
( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) by A3, A4, Def9;
hence [x,y] in OpenProd (S,A,B) by A4, A2, A5, Def9; :: thesis:

end;

assume A6: [x,y] in OpenProd (S,A,B) ; :: thesis:
A7: ( x in Day (S,A) & y in Day (S,A) ) by A6, ZFMISC_1:87;
A8: ( born (R,x) = born (S,x) & born (R,y) = born (S,y) ) by A1, A7, Th11;
( ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) = A & born (S,y) in B ) or ( born (S,x) in B & born (S,y) = A ) ) by A6, A7, Def9;
hence [x,y] in OpenProd (R,A,B) by A7, A2, A8, Def9; :: thesis:

end;

theorem Th15: :: SURREAL0:15

for A, B being Ordinal
for R, S being Relation st R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
ClosedProd (R,A,B) = ClosedProd (S,A,B)

let A, B be Ordinal; :: thesis:
let R, S be Relation; :: thesis:
assume A1: R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis:
A2: Day (R,A) = Day (S,A) by A1, Th10;
let x, y be object ; :: according to RELAT_1:def 2 :: thesis:
thus ( [x,y] in ClosedProd (R,A,B) implies [x,y] in ClosedProd (S,A,B) ) :: thesis:

assume A3: [x,y] in ClosedProd (R,A,B) ; :: thesis:
A4: ( x in Day (R,A) & y in Day (R,A) ) by A3, ZFMISC_1:87;
A5: ( born (R,x) = born (S,x) & born (R,y) = born (S,y) ) by A1, A4, Th11;
( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) by A3, A4, Def10;
hence [x,y] in ClosedProd (S,A,B) by A4, A2, A5, Def10; :: thesis:

end;

assume A6: [x,y] in ClosedProd (S,A,B) ; :: thesis:
A7: ( x in Day (S,A) & y in Day (S,A) ) by A6, ZFMISC_1:87;
A8: ( born (R,x) = born (S,x) & born (R,y) = born (S,y) ) by A1, A7, Th11;
( ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) = A & born (S,y) c= B ) or ( born (S,x) c= B & born (S,y) = A ) ) by A6, A7, Def10;
hence [x,y] in ClosedProd (R,A,B) by A7, A2, A8, Def10; :: thesis:

end;

theorem Th16: :: SURREAL0:16

for A, B being Ordinal
for R being Relation holds OpenProd (R,A,B) c= ClosedProd (R,A,B)

let A, B be Ordinal; :: thesis:
let R be Relation; :: thesis:
let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A1: [x,y] in OpenProd (R,A,B) ; :: thesis:
then A2: ( x in Day (R,A) & y in Day (R,A) ) by ZFMISC_1:87;
then ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) by A1, Def9;
then ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) by ORDINAL1:def 2;
hence [x,y] in ClosedProd (R,A,B) by A2, Def10; :: thesis:

end;

theorem Th17: :: SURREAL0:17

for A1, A2, B1, B2 being Ordinal
for R being Relation st ( A1 in A2 or ( A1 = A2 & B1 c= B2 ) ) holds
ClosedProd (R,A1,B1) c= ClosedProd (R,A2,B2)

let A1, A2, B1, B2 be Ordinal; :: thesis:
let R be Relation; :: thesis:
assume A1: ( A1 in A2 or ( A1 = A2 & B1 c= B2 ) ) ; :: thesis:
A2: A1 c= A2 by A1, ORDINAL1:def 2;
A3: Day (R,A1) c= Day (R,A2) by Th9, A1, ORDINAL1:def 2;
let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A4: [x,y] in ClosedProd (R,A1,B1) ; :: thesis:
A5: ( x in Day (R,A1) & y in Day (R,A1) ) by A4, ZFMISC_1:87;

per cases by A5, A4, Def10;

suppose ( born (R,x) in A1 & born (R,y) in A1 ) ; :: thesis:

hence [x,y] in ClosedProd (R,A2,B2) by A2, A3, A5, Def10; :: thesis:

end;

suppose A6: ( born (R,x) = A1 & born (R,y) c= B1 ) ; :: thesis:

per cases by A1;

suppose A7: A1 in A2 ; :: thesis:

born (R,y) c= A1 by A5, Def8;
then born (R,y) in A2 by A7, ORDINAL1:12;
hence [x,y] in ClosedProd (R,A2,B2) by A6, A7, A5, A3, Def10; :: thesis:

end;

suppose ( A1 = A2 & B1 c= B2 ) ; :: thesis:

then ( born (R,x) = A2 & born (R,y) c= B2 ) by A6, XBOOLE_1:1;
hence [x,y] in ClosedProd (R,A2,B2) by A5, A3, Def10; :: thesis:

end;

suppose A8: ( born (R,x) c= B1 & born (R,y) = A1 ) ; :: thesis:

per cases by A1;

suppose A9: A1 in A2 ; :: thesis:

born (R,x) c= A1 by A5, Def8;
then born (R,x) in A2 by A9, ORDINAL1:12;
hence [x,y] in ClosedProd (R,A2,B2) by A8, A9, A5, A3, Def10; :: thesis:

end;

suppose ( A1 = A2 & B1 c= B2 ) ; :: thesis:

then ( born (R,y) = A2 & born (R,x) c= B2 ) by A8, XBOOLE_1:1;
hence [x,y] in ClosedProd (R,A2,B2) by A5, A3, Def10; :: thesis:

end;

theorem Th18: :: SURREAL0:18

for A, B, C being Ordinal
for R being Relation st B in C holds
ClosedProd (R,A,B) c= OpenProd (R,A,C)

let A, B, C be Ordinal; :: thesis:
let R be Relation; :: thesis:
assume A1: B in C ; :: thesis:
let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A2: [x,y] in ClosedProd (R,A,B) ; :: thesis:
A3: ( x in Day (R,A) & y in Day (R,A) ) by A2, ZFMISC_1:87;
then ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) by A2, Def10;
then ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in C ) or ( born (R,x) in C & born (R,y) = A ) ) by A1, ORDINAL1:12;
hence [x,y] in OpenProd (R,A,C) by A3, Def9; :: thesis:

end;

theorem Th19: :: SURREAL0:19

for A, B being Ordinal
for R being Relation st A in B holds
ClosedProd (R,A,B) c= OpenProd (R,A,B)

let A, B be Ordinal; :: thesis:
let R be Relation; :: thesis:
assume A1: A in B ; :: thesis:
let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A2: [x,y] in ClosedProd (R,A,B) ; :: thesis:
then A3: ( x in Day (R,A) & y in Day (R,A) ) by ZFMISC_1:87;
( born (R,x) c= A & born (R,y) c= A ) by A3, Def8;
then A4: ( born (R,x) in B & born (R,y) in B ) by A1, ORDINAL1:12;
( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) by A3, A2, Def10;
hence [x,y] in OpenProd (R,A,B) by A3, A4, Def9; :: thesis:

end;

definition

let X, R be set ;

pred R preserves_No_Comparison_on X means :: SURREAL0:def 11
for a, b being object st [a,b] in X holds
( a <= R,b iff ( L_ a << R,{b} & {a} << R, R_ b ) );

end;

:: deftheorem defines preserves_No_Comparison_on SURREAL0:def 11 :

theorem Th20: :: SURREAL0:20

for A, B being Ordinal
for R, S being Relation st R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) holds
R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):]

let A, B be Ordinal; :: thesis:
let R, S be Relation; :: thesis:
assume that
A1: ( R is almost-No-order & S is almost-No-order ) and
A2: R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) ; :: thesis:
consider R0 being Ordinal such that
A3: R c= [:(Day (R,R0)),(Day (R,R0)):] by A1;
consider S0 being Ordinal such that
A4: S c= [:(Day (S,S0)),(Day (S,S0)):] by A1;
let y, z be object ; :: according to RELAT_1:def 2 :: thesis:
thus ( [y,z] in R /\ [:(BeforeGames A),(BeforeGames A):] implies [y,z] in S /\ [:(BeforeGames A),(BeforeGames A):] ) :: thesis:

assume [y,z] in R /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis:
then A5: ( [y,z] in R & [y,z] in [:(BeforeGames A),(BeforeGames A):] ) by XBOOLE_0:def 4;
then A6: ( y in BeforeGames A & z in BeforeGames A ) by ZFMISC_1:87;
A7: ( y in Day (R,R0) & z in Day (R,R0) ) by A3, A5, ZFMISC_1:87;
( y in BeforeGames A & z in BeforeGames A ) by A5, ZFMISC_1:87;
then consider Ay being Ordinal such that
A8: ( Ay in A & y in Games Ay ) by Def5;
consider Az being Ordinal such that
A9: ( Az in A & z in Games Az ) by A6, Def5;
A10: ( Day (R,Ay) c= Day (R,A) & Day (R,Az) c= Day (R,A) ) by Th9, A8, A9, ORDINAL1:def 2;
A11: ( y in Day (R,Ay) & z in Day (R,Az) ) by A8, A7, A9, Th12;
then ( born (R,y) c= Ay & born (R,z) c= Az ) by Def8;
then A12: ( born (R,y) in A & born (R,z) in A ) by A8, A9, ORDINAL1:12;
[y,z] in OpenProd (R,A,B) by A10, A11, A12, Def9;
then [y,z] in R /\ (OpenProd (R,A,B)) by XBOOLE_0:def 4, A5;
then [y,z] in S by A2, XBOOLE_0:def 4;
hence [y,z] in S /\ [:(BeforeGames A),(BeforeGames A):] by A5, XBOOLE_0:def 4; :: thesis:

end;

assume [y,z] in S /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis:
then A13: ( [y,z] in S & [y,z] in [:(BeforeGames A),(BeforeGames A):] ) by XBOOLE_0:def 4;
then A14: ( y in BeforeGames A & z in BeforeGames A ) by ZFMISC_1:87;
A15: ( y in Day (S,S0) & z in Day (S,S0) ) by A4, A13, ZFMISC_1:87;
consider Ay being Ordinal such that
A16: ( Ay in A & y in Games Ay ) by A14, Def5;
consider Az being Ordinal such that
A17: ( Az in A & z in Games Az ) by A14, Def5;
A18: ( Day (S,Ay) c= Day (S,A) & Day (S,Az) c= Day (S,A) ) by Th9, A16, A17, ORDINAL1:def 2;
A19: ( y in Day (S,Ay) & z in Day (S,Az) ) by A16, A15, A17, Th12;
then ( born (S,y) c= Ay & born (S,z) c= Az ) by Def8;
then A20: ( born (S,y) in A & born (S,z) in A ) by A16, A17, ORDINAL1:12;
[y,z] in OpenProd (S,A,B) by A18, A19, A20, Def9;
then [y,z] in S /\ (OpenProd (S,A,B)) by XBOOLE_0:def 4, A13;
then [y,z] in R by A2, XBOOLE_0:def 4;
hence [y,z] in R /\ [:(BeforeGames A),(BeforeGames A):] by A13, XBOOLE_0:def 4; :: thesis:

end;

Lm2: for A, B being Ordinal st B c= A holds
for R, S being Relation st R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) holds
R /\ (ClosedProd (R,A,B)) c= S /\ (ClosedProd (S,A,B))

let A, B be Ordinal; :: thesis:
assume A1: B c= A ; :: thesis:
let R, S be Relation; :: thesis:
assume that
A2: ( R is almost-No-order & S is almost-No-order ) and
A3: R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) and
A4: ( R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) ) ; :: thesis:
A5: S /\ [:(BeforeGames A),(BeforeGames A):] = R /\ [:(BeforeGames A),(BeforeGames A):] by Th20, A2, A3;
let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
A6: ( OpenProd (R,A,B) c= ClosedProd (R,A,B) & OpenProd (S,A,B) c= ClosedProd (S,A,B) ) by Th16;
assume A7: [x,y] in R /\ (ClosedProd (R,A,B)) ; :: thesis:
then A8: ( [x,y] in R & [x,y] in ClosedProd (R,A,B) ) by XBOOLE_0:def 4;
reconsider x = x, y = y as Element of Day (R,A) by ZFMISC_1:87, A7;
x <= R,y by A7, XBOOLE_0:def 4;
then A9: ( L_ x << R,{y} & {x} << R, R_ y ) by A8, A4;
A10: [x,y] in ClosedProd (R,A,B) by A7, XBOOLE_0:def 4;

per cases by Def10;

suppose ( born (R,x) in A & born (R,y) in A ) ; :: thesis:

then [x,y] in OpenProd (R,A,B) by Def9;
then [x,y] in S /\ (OpenProd (S,A,B)) by A3, A8, XBOOLE_0:def 4;
then ( [x,y] in S & [x,y] in OpenProd (S,A,B) ) by XBOOLE_0:def 4;
hence [x,y] in S /\ (ClosedProd (S,A,B)) by A6, XBOOLE_0:def 4; :: thesis:

end;

suppose A11: ( born (R,x) = A & born (R,y) c= B ) ; :: thesis:

suppose A12: born (R,y) = B ; :: thesis:

A13: Day (R,A) = Day (S,A) by A5, Th10;
A14: ClosedProd (R,A,B) = ClosedProd (S,A,B) by A5, Th15;
A15: L_ x << S,{y}

given l, r being object such that A16: ( l in L_ x & r in {y} & l >= S,r ) ; :: according to SURREAL0:def 3 :: thesis:
A17: r = y by A16, TARSKI:def 1;
l in (L_ x) \/ (R_ x) by A16, XBOOLE_0:def 3;
then consider O being Ordinal such that
A18: ( O in A & l in Day (R,O) ) by Th7;
A19: ( Day (S,O) = Day (R,O) & Day (R,O) c= Day (R,A) ) by Th9, A5, Th10, A18, ORDINAL1:def 2;
born (S,l) c= O by A18, A19, Def8;
then A20: born (S,l) in A by ORDINAL1:12, A18;
A21: born (S,y) = B by A12, Th11, A5;
[y,l] in OpenProd (S,A,B)

suppose A = B ; :: thesis:

hence [y,l] in OpenProd (S,A,B) by A20, Def9, A19, A18, A13, A21; :: thesis:

end;

suppose A <> B ; :: thesis:

then B in A by ORDINAL1:11, A1, XBOOLE_0:def 8;
hence [y,l] in OpenProd (S,A,B) by A20, Def9, A19, A18, A13, A21; :: thesis:

end;

then [y,l] in R /\ (OpenProd (R,A,B)) by A3, A16, A17, XBOOLE_0:def 4;
then l >= R,r by A17, XBOOLE_0:def 4;
hence contradiction by A9, A16; :: thesis:

end;

A22: {x} << S, R_ y

given l, r being object such that A23: ( l in {x} & r in R_ y & l >= S,r ) ; :: according to SURREAL0:def 3 :: thesis:
A24: l = x by A23, TARSKI:def 1;
A25: y in Day (R,B) by A12, Def8;
r in (L_ y) \/ (R_ y) by A23, XBOOLE_0:def 3;
then consider O being Ordinal such that
A26: ( O in B & r in Day (R,O) ) by A25, Th7;
A27: ( Day (S,O) = Day (R,O) & Day (R,O) c= Day (R,A) & Day (R,A) = Day (S,A) ) by Th9, A5, Th10, A1, A26, ORDINAL1:def 2;
born (S,r) c= O by A26, A27, Def8;
then A28: born (S,r) in B by A26, ORDINAL1:12;
born (S,x) = A by A11, Th11, A5;
then [r,x] in OpenProd (S,A,B) by A28, Def9, A27, A26;
then [r,x] in S /\ (OpenProd (S,A,B)) by A23, A24, XBOOLE_0:def 4;
then l >= R,r by A24, A3, XBOOLE_0:def 4;
hence contradiction by A9, A23; :: thesis:

end;

x <= S,y by A15, A22, A4, A14, A10;
hence [x,y] in S /\ (ClosedProd (S,A,B)) by A14, A10, XBOOLE_0:def 4; :: thesis:

end;

suppose born (R,y) <> B ; :: thesis:

then born (R,y) in B by A11, XBOOLE_0:def 8, ORDINAL1:11;
then [x,y] in OpenProd (R,A,B) by A11, Def9;
then [x,y] in R /\ (OpenProd (R,A,B)) by A8, XBOOLE_0:def 4;
then ( [x,y] in S & [x,y] in OpenProd (S,A,B) ) by A3, XBOOLE_0:def 4;
hence [x,y] in S /\ (ClosedProd (S,A,B)) by A6, XBOOLE_0:def 4; :: thesis:

end;

suppose A29: ( born (R,y) = A & born (R,x) c= B ) ; :: thesis:

suppose A30: born (R,x) = B ; :: thesis:

A31: Day (R,A) = Day (S,A) by A5, Th10;
A32: ClosedProd (R,A,B) = ClosedProd (S,A,B) by A5, Th15;
A33: L_ x << S,{y}

given l, r being object such that A34: ( l in L_ x & r in {y} & l >= S,r ) ; :: according to SURREAL0:def 3 :: thesis:
A35: r = y by A34, TARSKI:def 1;
A36: x in Day (R,B) by A30, Def8;
l in (L_ x) \/ (R_ x) by A34, XBOOLE_0:def 3;
then consider O being Ordinal such that
A37: ( O in B & l in Day (R,O) ) by A36, Th7;
A38: ( Day (S,O) = Day (R,O) & Day (R,O) c= Day (R,A) & Day (R,A) = Day (S,A) ) by Th9, A5, Th10, A1, A37, ORDINAL1:def 2;
born (S,l) c= O by A37, A38, Def8;
then A39: born (S,l) in B by A37, ORDINAL1:12;
born (S,y) = A by A29, Th11, A5;
then [y,l] in OpenProd (S,A,B) by A39, Def9, A37, A38;
then [y,l] in R /\ (OpenProd (R,A,B)) by A3, A34, A35, XBOOLE_0:def 4;
then l >= R,r by A35, XBOOLE_0:def 4;
hence contradiction by A9, A34; :: thesis:

end;

A40: {x} << S, R_ y

given l, r being object such that A41: ( l in {x} & r in R_ y & l >= S,r ) ; :: according to SURREAL0:def 3 :: thesis:
A42: l = x by A41, TARSKI:def 1;
r in (L_ y) \/ (R_ y) by A41, XBOOLE_0:def 3;
then consider O being Ordinal such that
A43: ( O in A & r in Day (R,O) ) by Th7;
A44: ( Day (S,O) = Day (R,O) & Day (R,O) c= Day (R,A) ) by Th9, A5, Th10, A43, ORDINAL1:def 2;
born (S,r) c= O by A43, A44, Def8;
then A45: born (S,r) in A by ORDINAL1:12, A43;
A46: born (S,x) = B by A30, Th11, A5;
[r,x] in OpenProd (S,A,B)

suppose A = B ; :: thesis:

hence [r,x] in OpenProd (S,A,B) by A45, A31, Def9, A44, A43, A46; :: thesis:

end;

suppose A <> B ; :: thesis:

then B in A by ORDINAL1:11, A1, XBOOLE_0:def 8;
hence [r,x] in OpenProd (S,A,B) by A45, A31, Def9, A44, A43, A46; :: thesis:

end;

then [r,x] in S /\ (OpenProd (S,A,B)) by A41, A42, XBOOLE_0:def 4;
then l >= R,r by A3, A42, XBOOLE_0:def 4;
hence contradiction by A9, A41; :: thesis:

end;

x <= S,y by A32, A10, A33, A40, A4;
hence [x,y] in S /\ (ClosedProd (S,A,B)) by A32, A10, XBOOLE_0:def 4; :: thesis:

end;

suppose born (R,x) <> B ; :: thesis:

then born (R,x) in B by ORDINAL1:11, A29, XBOOLE_0:def 8;
then [x,y] in OpenProd (R,A,B) by A29, Def9;
then [x,y] in R /\ (OpenProd (R,A,B)) by A8, XBOOLE_0:def 4;
then ( [x,y] in S & [x,y] in OpenProd (S,A,B) ) by A3, XBOOLE_0:def 4;
hence [x,y] in S /\ (ClosedProd (S,A,B)) by A6, XBOOLE_0:def 4; :: thesis:

end;

theorem Th21: :: SURREAL0:21

for A, B being Ordinal
for R, S being Relation st R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) holds
R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B))

let A, B be Ordinal; :: thesis:
let R, S be Relation; :: thesis:
assume A1: ( R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) ) ; :: thesis:

suppose B c= A ; :: thesis:

then ( R /\ (ClosedProd (R,A,B)) c= S /\ (ClosedProd (S,A,B)) & S /\ (ClosedProd (S,A,B)) c= R /\ (ClosedProd (R,A,B)) ) by A1, Lm2;
hence R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B)) by XBOOLE_0:def 10; :: thesis:

end;

suppose A in B ; :: thesis:

then ( ClosedProd (R,A,B) c= OpenProd (R,A,B) & OpenProd (R,A,B) c= ClosedProd (R,A,B) & ClosedProd (S,A,B) c= OpenProd (S,A,B) & OpenProd (S,A,B) c= ClosedProd (S,A,B) ) by Th16, Th19;
then ( ClosedProd (R,A,B) = OpenProd (R,A,B) & ClosedProd (S,A,B) = OpenProd (S,A,B) ) by XBOOLE_0:def 10;
hence R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B)) by A1; :: thesis:

end;

theorem Th22: :: SURREAL0:22

for A, B being Ordinal
for R, S being Relation st R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,0)) = S /\ (OpenProd (S,A,0)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) holds
R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B))

let A, B be Ordinal; :: thesis:
let R, S be Relation; :: thesis:
assume that
A1: ( R is almost-No-order & S is almost-No-order ) and
A2: R /\ (OpenProd (R,A,0)) = S /\ (OpenProd (S,A,0)) and
A3: ( R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) ) ; :: thesis:
defpred S₁[ Ordinal] means ( $1 c= B implies R /\ (ClosedProd (R,A,$1)) = S /\ (ClosedProd (S,A,$1)) );
A4: R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] by A1, A2, Th20;
A5: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

let D be Ordinal; :: thesis:
assume A6: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:
assume A7: D c= B ; :: thesis:
then ( ClosedProd (R,A,D) c= ClosedProd (R,A,B) & ClosedProd (S,A,D) c= ClosedProd (S,A,B) ) by Th17;
then A8: ( R preserves_No_Comparison_on ClosedProd (R,A,D) & S preserves_No_Comparison_on ClosedProd (S,A,D) ) by A3;
A9: R /\ (OpenProd (R,A,D)) c= S /\ (OpenProd (S,A,D))

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A10: [x,y] in R /\ (OpenProd (R,A,D)) ; :: thesis:
then A11: ( [x,y] in R & [x,y] in OpenProd (R,A,D) ) by XBOOLE_0:def 4;
A12: ( x in Day (R,A) & y in Day (R,A) ) by ZFMISC_1:87, A10;
then A13: ( born (R,x) = born (S,x) & born (R,y) = born (S,y) ) by A4, Th11;

per cases by A11, A12, Def9;

suppose ( born (R,x) in A & born (R,y) in A ) ; :: thesis:

then [x,y] in OpenProd (R,A,0) by A12, Def9;
then A14: [x,y] in S /\ (OpenProd (S,A,0)) by A2, A11, XBOOLE_0:def 4;
then A15: ( [x,y] in S & [x,y] in OpenProd (S,A,0) ) by XBOOLE_0:def 4;
A16: ( x in Day (S,A) & y in Day (S,A) ) by A14, ZFMISC_1:87;
then ( ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) = A & born (S,y) in {} ) or ( born (S,x) in {} & born (S,y) = A ) ) by A15, Def9;
then [x,y] in OpenProd (S,A,D) by A16, Def9;
hence [x,y] in S /\ (OpenProd (S,A,D)) by A15, XBOOLE_0:def 4; :: thesis:

end;

suppose A17: ( born (R,x) = A & born (R,y) in D ) ; :: thesis:

then [x,y] in ClosedProd (R,A,(born (R,y))) by A12, Def10;
then A18: [x,y] in R /\ (ClosedProd (R,A,(born (R,y)))) by A11, XBOOLE_0:def 4;
A19: ClosedProd (S,A,(born (R,y))) c= OpenProd (S,A,D) by Th18, A17;
[x,y] in S /\ (ClosedProd (S,A,(born (R,y)))) by A7, A17, A6, A18, ORDINAL1:def 2;
then ( [x,y] in S & [x,y] in ClosedProd (S,A,(born (S,y))) ) by A13, XBOOLE_0:def 4;
hence [x,y] in S /\ (OpenProd (S,A,D)) by A19, A13, XBOOLE_0:def 4; :: thesis:

end;

suppose A20: ( born (R,x) in D & born (R,y) = A ) ; :: thesis:

then [x,y] in ClosedProd (R,A,(born (R,x))) by A12, Def10;
then A21: [x,y] in R /\ (ClosedProd (R,A,(born (R,x)))) by A11, XBOOLE_0:def 4;
A22: ClosedProd (S,A,(born (R,x))) c= OpenProd (S,A,D) by Th18, A20;
[x,y] in S /\ (ClosedProd (S,A,(born (R,x)))) by A7, A20, A6, A21, ORDINAL1:def 2;
then ( [x,y] in S & [x,y] in ClosedProd (S,A,(born (S,x))) ) by A13, XBOOLE_0:def 4;
hence [x,y] in S /\ (OpenProd (S,A,D)) by XBOOLE_0:def 4, A22, A13; :: thesis:

end;

S /\ (OpenProd (S,A,D)) c= R /\ (OpenProd (R,A,D))

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A23: [x,y] in S /\ (OpenProd (S,A,D)) ; :: thesis:
then A24: ( [x,y] in S & [x,y] in OpenProd (S,A,D) ) by XBOOLE_0:def 4;
A25: ( x in Day (S,A) & y in Day (S,A) ) by ZFMISC_1:87, A23;
then A26: ( born (R,x) = born (S,x) & born (R,y) = born (S,y) ) by A4, Th11;

per cases by A24, A25, Def9;

suppose ( born (S,x) in A & born (S,y) in A ) ; :: thesis:

then [x,y] in OpenProd (S,A,0) by A25, Def9;
then A27: [x,y] in R /\ (OpenProd (R,A,0)) by A2, A24, XBOOLE_0:def 4;
then A28: ( [x,y] in R & [x,y] in OpenProd (R,A,0) ) by XBOOLE_0:def 4;
A29: ( x in Day (R,A) & y in Day (R,A) ) by A27, ZFMISC_1:87;
then ( born (R,x) in A & born (R,y) in A ) by A28, Def9;
then [x,y] in OpenProd (R,A,D) by A29, Def9;
hence [x,y] in R /\ (OpenProd (R,A,D)) by A28, XBOOLE_0:def 4; :: thesis:

end;

suppose A30: ( born (S,x) = A & born (S,y) in D ) ; :: thesis:

then [x,y] in ClosedProd (S,A,(born (S,y))) by A25, Def10;
then A31: [x,y] in S /\ (ClosedProd (S,A,(born (S,y)))) by A24, XBOOLE_0:def 4;
A32: ClosedProd (R,A,(born (S,y))) c= OpenProd (R,A,D) by Th18, A30;
[x,y] in R /\ (ClosedProd (R,A,(born (R,y)))) by A26, A6, A30, A31, A7, ORDINAL1:def 2;
then ( [x,y] in R & [x,y] in ClosedProd (R,A,(born (R,y))) ) by XBOOLE_0:def 4;
hence [x,y] in R /\ (OpenProd (R,A,D)) by A32, A26, XBOOLE_0:def 4; :: thesis:

end;

suppose A33: ( born (S,x) in D & born (S,y) = A ) ; :: thesis:

then [x,y] in ClosedProd (S,A,(born (S,x))) by A25, Def10;
then A34: [x,y] in S /\ (ClosedProd (S,A,(born (S,x)))) by A24, XBOOLE_0:def 4;
A35: ClosedProd (R,A,(born (S,x))) c= OpenProd (R,A,D) by Th18, A33;
[x,y] in R /\ (ClosedProd (R,A,(born (S,x)))) by A7, A33, A6, A34, ORDINAL1:def 2;
then ( [x,y] in R & [x,y] in ClosedProd (R,A,(born (R,x))) ) by A26, XBOOLE_0:def 4;
hence [x,y] in R /\ (OpenProd (R,A,D)) by A35, A26, XBOOLE_0:def 4; :: thesis:

end;

hence R /\ (ClosedProd (R,A,D)) = S /\ (ClosedProd (S,A,D)) by A1, A8, Th21, A9, XBOOLE_0:def 10; :: thesis:

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A5);
hence R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B)) ; :: thesis:

end;

theorem Th23: :: SURREAL0:23

for A, B being Ordinal
for R, S being Relation st R is almost-No-order & S is almost-No-order & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) holds
R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B))

let A, B be Ordinal; :: thesis:
let R, S be Relation; :: thesis:
assume A1: ( R is almost-No-order & S is almost-No-order & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) ) ; :: thesis:
defpred S₁[ Ordinal] means ( $1 in A implies R /\ (ClosedProd (R,$1,$1)) = S /\ (ClosedProd (S,$1,$1)) );
A2: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

let D be Ordinal; :: thesis:
assume A3: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:
assume A4: D in A ; :: thesis:
( ClosedProd (R,D,D) c= ClosedProd (R,A,B) & ClosedProd (S,D,D) c= ClosedProd (S,A,B) ) by A4, Th17;
then A5: ( R preserves_No_Comparison_on ClosedProd (R,D,D) & S preserves_No_Comparison_on ClosedProd (S,D,D) ) by A1;
A6: R /\ (OpenProd (R,D,0)) c= S /\ (OpenProd (S,D,0))

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A7: [x,y] in R /\ (OpenProd (R,D,0)) ; :: thesis:
A8: ( [x,y] in R & [x,y] in OpenProd (R,D,0) ) by A7, XBOOLE_0:def 4;
A9: ( x in Day (R,D) & y in Day (R,D) ) by A7, ZFMISC_1:87;
then A10: ( born (R,x) in D & born (R,y) in D ) by A8, Def9;
A11: ( x in Day (R,(born (R,x))) & y in Day (R,(born (R,y))) ) by A9, Def8;
A12: ( born (R,x) in A & born (R,y) in A ) by A10, A4, ORDINAL1:10;

suppose A13: born (R,x) c= born (R,y) ; :: thesis:

set b = born (R,y);
Day (R,(born (R,x))) c= Day (R,(born (R,y))) by A13, Th9;
then [x,y] in ClosedProd (R,(born (R,y)),(born (R,y))) by A11, Def10, A13;
then [x,y] in R /\ (ClosedProd (R,(born (R,y)),(born (R,y)))) by A8, XBOOLE_0:def 4;
then A14: [x,y] in S /\ (ClosedProd (S,(born (R,y)),(born (R,y)))) by A10, A12, A3;
then A15: ( [x,y] in S & [x,y] in ClosedProd (S,(born (R,y)),(born (R,y))) ) by XBOOLE_0:def 4;
A16: ( x in Day (S,(born (R,y))) & y in Day (S,(born (R,y))) ) by A14, ZFMISC_1:87;
A17: Day (S,(born (R,y))) c= Day (S,D) by A10, ORDINAL1:def 2, Th9;
( ( born (S,x) in born (R,y) & born (S,y) in born (R,y) ) or ( born (S,x) = born (R,y) & born (S,y) c= born (R,y) ) or ( born (S,x) c= born (R,y) & born (S,y) = born (R,y) ) ) by A15, A16, Def10;
then ( ( born (S,x) in D & born (S,y) in D ) or ( born (S,x) in D & born (S,y) in D ) or ( born (S,x) in D & born (S,y) in D ) ) by A10, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (S,D,0) by A17, A16, Def9;
hence [x,y] in S /\ (OpenProd (S,D,0)) by A15, XBOOLE_0:def 4; :: thesis:

end;

suppose A18: born (R,y) in born (R,x) ; :: thesis:

then A19: born (R,y) c= born (R,x) by ORDINAL1:def 2;
set b = born (R,x);
Day (R,(born (R,y))) c= Day (R,(born (R,x))) by A18, ORDINAL1:def 2, Th9;
then [x,y] in ClosedProd (R,(born (R,x)),(born (R,x))) by A11, Def10, A19;
then [x,y] in R /\ (ClosedProd (R,(born (R,x)),(born (R,x)))) by A8, XBOOLE_0:def 4;
then A20: [x,y] in S /\ (ClosedProd (S,(born (R,x)),(born (R,x)))) by A10, A12, A3;
then A21: ( [x,y] in S & [x,y] in ClosedProd (S,(born (R,x)),(born (R,x))) ) by XBOOLE_0:def 4;
A22: ( x in Day (S,(born (R,x))) & y in Day (S,(born (R,x))) ) by ZFMISC_1:87, A20;
A23: Day (S,(born (R,x))) c= Day (S,D) by A10, ORDINAL1:def 2, Th9;
( ( born (S,x) in born (R,x) & born (S,y) in born (R,x) ) or ( born (S,x) = born (R,x) & born (S,y) c= born (R,x) ) or ( born (S,x) c= born (R,x) & born (S,y) = born (R,x) ) ) by A21, A22, Def10;
then ( ( born (S,x) in D & born (S,y) in D ) or ( born (S,x) in D & born (S,y) in D ) or ( born (S,x) in D & born (S,y) in D ) ) by A10, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (S,D,0) by A23, A22, Def9;
hence [x,y] in S /\ (OpenProd (S,D,0)) by A21, XBOOLE_0:def 4; :: thesis:

end;

S /\ (OpenProd (S,D,0)) c= R /\ (OpenProd (R,D,0))

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A24: [x,y] in S /\ (OpenProd (S,D,0)) ; :: thesis:
A25: ( [x,y] in S & [x,y] in OpenProd (S,D,0) ) by A24, XBOOLE_0:def 4;
A26: ( x in Day (S,D) & y in Day (S,D) ) by A24, ZFMISC_1:87;
then A27: ( born (S,x) in D & born (S,y) in D ) by A25, Def9;
A28: ( x in Day (S,(born (S,x))) & y in Day (S,(born (S,y))) ) by A26, Def8;
A29: ( born (S,x) in A & born (S,y) in A ) by A27, A4, ORDINAL1:10;

suppose A30: born (S,x) c= born (S,y) ; :: thesis:

set b = born (S,y);
Day (S,(born (S,x))) c= Day (S,(born (S,y))) by A30, Th9;
then [x,y] in ClosedProd (S,(born (S,y)),(born (S,y))) by A28, Def10, A30;
then [x,y] in S /\ (ClosedProd (S,(born (S,y)),(born (S,y)))) by A25, XBOOLE_0:def 4;
then A31: [x,y] in R /\ (ClosedProd (R,(born (S,y)),(born (S,y)))) by A27, A29, A3;
then A32: ( [x,y] in R & [x,y] in ClosedProd (R,(born (S,y)),(born (S,y))) ) by XBOOLE_0:def 4;
A33: ( x in Day (R,(born (S,y))) & y in Day (R,(born (S,y))) ) by A31, ZFMISC_1:87;
A34: Day (R,(born (S,y))) c= Day (R,D) by A27, ORDINAL1:def 2, Th9;
( ( born (R,x) in born (S,y) & born (R,y) in born (S,y) ) or ( born (R,x) = born (S,y) & born (R,y) c= born (S,y) ) or ( born (R,x) c= born (S,y) & born (R,y) = born (S,y) ) ) by A32, A33, Def10;
then ( ( born (R,x) in D & born (R,y) in D ) or ( born (R,x) in D & born (R,y) in D ) or ( born (R,x) in D & born (R,y) in D ) ) by A27, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (R,D,0) by A34, A33, Def9;
hence [x,y] in R /\ (OpenProd (R,D,0)) by A32, XBOOLE_0:def 4; :: thesis:

end;

suppose A35: born (S,y) in born (S,x) ; :: thesis:

then A36: born (S,y) c= born (S,x) by ORDINAL1:def 2;
set b = born (S,x);
Day (S,(born (S,y))) c= Day (S,(born (S,x))) by A35, ORDINAL1:def 2, Th9;
then [x,y] in ClosedProd (S,(born (S,x)),(born (S,x))) by A28, Def10, A36;
then [x,y] in S /\ (ClosedProd (S,(born (S,x)),(born (S,x)))) by A25, XBOOLE_0:def 4;
then A37: [x,y] in R /\ (ClosedProd (R,(born (S,x)),(born (S,x)))) by A27, A29, A3;
then A38: ( [x,y] in R & [x,y] in ClosedProd (R,(born (S,x)),(born (S,x))) ) by XBOOLE_0:def 4;
A39: ( x in Day (R,(born (S,x))) & y in Day (R,(born (S,x))) ) by ZFMISC_1:87, A37;
A40: Day (R,(born (S,x))) c= Day (R,D) by A27, ORDINAL1:def 2, Th9;
( ( born (R,x) in born (S,x) & born (R,y) in born (S,x) ) or ( born (R,x) = born (S,x) & born (R,y) c= born (S,x) ) or ( born (R,x) c= born (S,x) & born (R,y) = born (S,x) ) ) by A38, A39, Def10;
then ( ( born (R,x) in D & born (R,y) in D ) or ( born (R,x) in D & born (R,y) in D ) or ( born (R,x) in D & born (R,y) in D ) ) by A27, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (R,D,0) by A40, A39, Def9;
hence [x,y] in R /\ (OpenProd (R,D,0)) by A38, XBOOLE_0:def 4; :: thesis:

end;

hence R /\ (ClosedProd (R,D,D)) = S /\ (ClosedProd (S,D,D)) by A1, A5, Th22, A6, XBOOLE_0:def 10; :: thesis:

end;

A41: for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A2);
A42: R /\ (OpenProd (R,A,0)) c= S /\ (OpenProd (S,A,0))

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A43: [x,y] in R /\ (OpenProd (R,A,0)) ; :: thesis:
A44: ( [x,y] in R & [x,y] in OpenProd (R,A,0) ) by A43, XBOOLE_0:def 4;
A45: ( x in Day (R,A) & y in Day (R,A) ) by ZFMISC_1:87, A43;
then A46: ( born (R,x) in A & born (R,y) in A ) by A44, Def9;
A47: ( x in Day (R,(born (R,x))) & y in Day (R,(born (R,y))) ) by A45, Def8;

suppose A48: born (R,x) c= born (R,y) ; :: thesis:

set b = born (R,y);
Day (R,(born (R,x))) c= Day (R,(born (R,y))) by A48, Th9;
then [x,y] in ClosedProd (R,(born (R,y)),(born (R,y))) by A47, Def10, A48;
then [x,y] in R /\ (ClosedProd (R,(born (R,y)),(born (R,y)))) by A44, XBOOLE_0:def 4;
then A49: [x,y] in S /\ (ClosedProd (S,(born (R,y)),(born (R,y)))) by A41, A46;
then A50: ( [x,y] in S & [x,y] in ClosedProd (S,(born (R,y)),(born (R,y))) ) by XBOOLE_0:def 4;
A51: ( x in Day (S,(born (R,y))) & y in Day (S,(born (R,y))) ) by A49, ZFMISC_1:87;
A52: Day (S,(born (R,y))) c= Day (S,A) by A46, ORDINAL1:def 2, Th9;
( ( born (S,x) in born (R,y) & born (S,y) in born (R,y) ) or ( born (S,x) = born (R,y) & born (S,y) c= born (R,y) ) or ( born (S,x) c= born (R,y) & born (S,y) = born (R,y) ) ) by A50, A51, Def10;
then ( ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) in A & born (S,y) in A ) ) by A46, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (S,A,0) by A52, A51, Def9;
hence [x,y] in S /\ (OpenProd (S,A,0)) by A50, XBOOLE_0:def 4; :: thesis:

end;

suppose A53: born (R,y) in born (R,x) ; :: thesis:

then A54: born (R,y) c= born (R,x) by ORDINAL1:def 2;
set b = born (R,x);
Day (R,(born (R,y))) c= Day (R,(born (R,x))) by A53, ORDINAL1:def 2, Th9;
then [x,y] in ClosedProd (R,(born (R,x)),(born (R,x))) by A47, Def10, A54;
then [x,y] in R /\ (ClosedProd (R,(born (R,x)),(born (R,x)))) by A44, XBOOLE_0:def 4;
then A55: [x,y] in S /\ (ClosedProd (S,(born (R,x)),(born (R,x)))) by A41, A46;
then A56: ( [x,y] in S & [x,y] in ClosedProd (S,(born (R,x)),(born (R,x))) ) by XBOOLE_0:def 4;
A57: ( x in Day (S,(born (R,x))) & y in Day (S,(born (R,x))) ) by A55, ZFMISC_1:87;
A58: Day (S,(born (R,x))) c= Day (S,A) by A46, ORDINAL1:def 2, Th9;
( ( born (S,x) in born (R,x) & born (S,y) in born (R,x) ) or ( born (S,x) = born (R,x) & born (S,y) c= born (R,x) ) or ( born (S,x) c= born (R,x) & born (S,y) = born (R,x) ) ) by A56, A57, Def10;
then ( ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) in A & born (S,y) in A ) or ( born (S,x) in A & born (S,y) in A ) ) by A46, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (S,A,0) by A58, A57, Def9;
hence [x,y] in S /\ (OpenProd (S,A,0)) by A56, XBOOLE_0:def 4; :: thesis:

end;

S /\ (OpenProd (S,A,0)) c= R /\ (OpenProd (R,A,0))

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A59: [x,y] in S /\ (OpenProd (S,A,0)) ; :: thesis:
A60: ( [x,y] in S & [x,y] in OpenProd (S,A,0) ) by A59, XBOOLE_0:def 4;
A61: ( x in Day (S,A) & y in Day (S,A) ) by A59, ZFMISC_1:87;
then A62: ( born (S,x) in A & born (S,y) in A ) by A60, Def9;
A63: ( x in Day (S,(born (S,x))) & y in Day (S,(born (S,y))) ) by A61, Def8;

suppose A64: born (S,x) c= born (S,y) ; :: thesis:

set b = born (S,y);
Day (S,(born (S,x))) c= Day (S,(born (S,y))) by A64, Th9;
then [x,y] in ClosedProd (S,(born (S,y)),(born (S,y))) by A63, Def10, A64;
then [x,y] in S /\ (ClosedProd (S,(born (S,y)),(born (S,y)))) by A60, XBOOLE_0:def 4;
then A65: [x,y] in R /\ (ClosedProd (R,(born (S,y)),(born (S,y)))) by A41, A62;
then A66: ( [x,y] in R & [x,y] in ClosedProd (R,(born (S,y)),(born (S,y))) ) by XBOOLE_0:def 4;
A67: ( x in Day (R,(born (S,y))) & y in Day (R,(born (S,y))) ) by A65, ZFMISC_1:87;
A68: Day (R,(born (S,y))) c= Day (R,A) by A62, ORDINAL1:def 2, Th9;
( ( born (R,x) in born (S,y) & born (R,y) in born (S,y) ) or ( born (R,x) = born (S,y) & born (R,y) c= born (S,y) ) or ( born (R,x) c= born (S,y) & born (R,y) = born (S,y) ) ) by A66, A67, Def10;
then ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) in A & born (R,y) in A ) ) by A62, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (R,A,0) by A68, A67, Def9;
hence [x,y] in R /\ (OpenProd (R,A,0)) by A66, XBOOLE_0:def 4; :: thesis:

end;

suppose A69: born (S,y) in born (S,x) ; :: thesis:

then A70: born (S,y) c= born (S,x) by ORDINAL1:def 2;
set b = born (S,x);
Day (S,(born (S,y))) c= Day (S,(born (S,x))) by A69, ORDINAL1:def 2, Th9;
then [x,y] in ClosedProd (S,(born (S,x)),(born (S,x))) by A63, Def10, A70;
then [x,y] in S /\ (ClosedProd (S,(born (S,x)),(born (S,x)))) by A60, XBOOLE_0:def 4;
then A71: [x,y] in R /\ (ClosedProd (R,(born (S,x)),(born (S,x)))) by A41, A62;
then A72: ( [x,y] in R & [x,y] in ClosedProd (R,(born (S,x)),(born (S,x))) ) by XBOOLE_0:def 4;
A73: ( x in Day (R,(born (S,x))) & y in Day (R,(born (S,x))) ) by A71, ZFMISC_1:87;
A74: Day (R,(born (S,x))) c= Day (R,A) by A62, ORDINAL1:def 2, Th9;
( ( born (R,x) in born (S,x) & born (R,y) in born (S,x) ) or ( born (R,x) = born (S,x) & born (R,y) c= born (S,x) ) or ( born (R,x) c= born (S,x) & born (R,y) = born (S,x) ) ) by A72, A73, Def10;
then ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) in A & born (R,y) in A ) ) by A62, ORDINAL1:10, ORDINAL1:12;
then [x,y] in OpenProd (R,A,0) by A74, A73, Def9;
hence [x,y] in R /\ (OpenProd (R,A,0)) by A72, XBOOLE_0:def 4; :: thesis:

end;

hence R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B)) by A1, Th22, A42, XBOOLE_0:def 10; :: thesis:

end;

theorem Th24: :: SURREAL0:24

for Lp, Lr being Sequence st dom Lp = dom Lr & ( for A being Ordinal st A in dom Lp holds
( ex a, b being Ordinal ex R being Relation st
( R = Lr . A & Lp . A = ClosedProd (R,a,b) ) & Lr . A is Relation & ( for R being Relation st R = Lr . A holds
( R preserves_No_Comparison_on Lp . A & R c= Lp . A ) ) ) ) holds
( union (rng Lr) is Relation & ( for R being Relation st R = union (rng Lr) holds
( R preserves_No_Comparison_on union (rng Lp) & R c= union (rng Lp) & ( for A, a, b being Ordinal
for S being Relation st A in dom Lp & S = Lr . A & Lp . A = ClosedProd (S,a,b) holds
R /\ [:(BeforeGames a),(BeforeGames a):] = S /\ [:(BeforeGames a),(BeforeGames a):] ) ) ) )

let Lp, Lr be Sequence; :: thesis:
assume that
A1: dom Lp = dom Lr and
A2: for A being Ordinal st A in dom Lp holds
( ex a, b being Ordinal ex R being Relation st
( R = Lr . A & Lp . A = ClosedProd (R,a,b) ) & Lr . A is Relation & ( for R being Relation st R = Lr . A holds
( R preserves_No_Comparison_on Lp . A & R c= Lp . A ) ) ) ; :: thesis:
union (rng Lr) is Relation-like

let y be object ; :: according to RELAT_1:def 1 :: thesis:
assume A3: y in union (rng Lr) ; :: thesis:
consider Y being set such that
A4: ( y in Y & Y in rng Lr ) by A3, TARSKI:def 4;
consider A being object such that
A5: ( A in dom Lr & Lr . A = Y ) by A4, FUNCT_1:def 3;
reconsider A = A as Ordinal by A5;
ex a, b being Ordinal ex R being Relation st
( R = Lr . A & Lp . A = ClosedProd (R,a,b) ) by A5, A2, A1;
hence ex b₁, b₂ being object st y = [b₁,b₂] by A4, A5, RELAT_1:def 1; :: thesis:

end;

hence union (rng Lr) is Relation ; :: thesis:
let R be Relation; :: thesis:
assume A6: R = union (rng Lr) ; :: thesis:
A7: R c= union (rng Lp)

let y, z be object ; :: according to RELAT_1:def 3 :: thesis:
assume A8: [y,z] in R ; :: thesis:
consider Y being set such that
A9: ( [y,z] in Y & Y in rng Lr ) by A6, A8, TARSKI:def 4;
consider A being object such that
A10: ( A in dom Lr & Lr . A = Y ) by A9, FUNCT_1:def 3;
reconsider A = A as Ordinal by A10;
reconsider R = Lr . A as Relation by A10, A1, A2;
( R c= Lp . A & Lp . A in rng Lp ) by A10, A1, A2, FUNCT_1:def 3;
hence [y,z] in union (rng Lp) by A9, A10, TARSKI:def 4; :: thesis:

end;

R preserves_No_Comparison_on union (rng Lp)

let x, y be object ; :: according to SURREAL0:def 11 :: thesis:
assume A11: [x,y] in union (rng Lp) ; :: thesis:
consider Y being set such that
A12: ( [x,y] in Y & Y in rng Lp ) by A11, TARSKI:def 4;
consider A being object such that
A13: ( A in dom Lp & Lp . A = Y ) by A12, FUNCT_1:def 3;
consider a, b being Ordinal, T being Relation such that
A14: ( T = Lr . A & Lp . A = ClosedProd (T,a,b) ) by A13, A2;
A15: ( T preserves_No_Comparison_on Lp . A & T c= Lp . A ) by A13, A14, A2;
thus ( x <= R,y implies ( L_ x << R,{y} & {x} << R, R_ y ) ) :: thesis:

assume x <= R,y ; :: thesis:
then consider Y being set such that
A16: ( [x,y] in Y & Y in rng Lr ) by A6, TARSKI:def 4;
consider A being object such that
A17: ( A in dom Lr & Lr . A = Y ) by A16, FUNCT_1:def 3;
consider a, b being Ordinal, S being Relation such that
A18: ( S = Lr . A & Lp . A = ClosedProd (S,a,b) ) by A17, A2, A1;
A19: ( S preserves_No_Comparison_on ClosedProd (S,a,b) & S c= ClosedProd (S,a,b) ) by A17, A18, A1, A2;
then A20: S is almost-No-order by XBOOLE_1:1;
x <= S,y by A16, A17, A18;
then A21: ( L_ x << S,{y} & {x} << S, R_ y ) by A19;
A22: L_ x << R,{y}

given l, r being object such that A23: ( l in L_ x & r in {y} & l >= R,r ) ; :: according to SURREAL0:def 3 :: thesis:
A24: not l >= S,r by A21, A23;
consider Z being set such that
A25: ( [r,l] in Z & Z in rng Lr ) by A23, A6, TARSKI:def 4;
consider B being object such that
A26: ( B in dom Lr & Lr . B = Z ) by A25, FUNCT_1:def 3;
consider a1, b1 being Ordinal, W being Relation such that
A27: ( W = Lr . B & Lp . B = ClosedProd (W,a1,b1) ) by A26, A2, A1;
A28: ( W preserves_No_Comparison_on ClosedProd (W,a1,b1) & W c= ClosedProd (W,a1,b1) ) by A26, A27, A1, A2;
then A29: W is almost-No-order by XBOOLE_1:1;

suppose ( a1 in a or ( a1 = a & b1 c= b ) ) ; :: thesis:

then ClosedProd (S,a1,b1) c= ClosedProd (S,a,b) by Th17;
then S preserves_No_Comparison_on ClosedProd (S,a1,b1) by A19;
then A30: S /\ (ClosedProd (S,a1,b1)) = W /\ (ClosedProd (W,a1,b1)) by A28, A20, A29, Th23;
[r,l] in W /\ (ClosedProd (W,a1,b1)) by A25, A26, A27, A28, XBOOLE_0:def 4;
hence contradiction by A24, A30, XBOOLE_0:def 4; :: thesis:

end;

suppose A31: ( not a1 in a & ( not a1 = a or not b1 c= b ) ) ; :: thesis:

then A32: a c= a1 by ORDINAL1:16;
( a in a1 or ( a = a1 & b c= b1 ) )

assume A33: ( not a in a1 & ( not a = a1 or not b c= b1 ) ) ; :: thesis:
then a1 c= a by ORDINAL1:16;
hence contradiction by A33, A31, A32, XBOOLE_0:def 10; :: thesis:

end;

then ClosedProd (W,a,b) c= ClosedProd (W,a1,b1) by Th17;
then W preserves_No_Comparison_on ClosedProd (W,a,b) by A28;
then A34: S /\ (ClosedProd (S,a,b)) = W /\ (ClosedProd (W,a,b)) by A19, A20, A29, Th23;
[x,y] in W /\ (ClosedProd (W,a,b)) by A34, A16, A17, A18, A19, XBOOLE_0:def 4;
then [x,y] in W by XBOOLE_0:def 4;
then ( x <= W,y & [x,y] in ClosedProd (W,a1,b1) ) by A28;
then L_ x << W,{y} by A28;
then not l >= W,r by A23;
hence contradiction by A25, A26, A27; :: thesis:

end;

{x} << R, R_ y

given l, r being object such that A35: ( l in {x} & r in R_ y & l >= R,r ) ; :: according to SURREAL0:def 3 :: thesis:
A36: not l >= S,r by A21, A35;
consider Z being set such that
A37: ( [r,l] in Z & Z in rng Lr ) by A35, A6, TARSKI:def 4;
consider B being object such that
A38: ( B in dom Lr & Lr . B = Z ) by A37, FUNCT_1:def 3;
consider a1, b1 being Ordinal, W being Relation such that
A39: ( W = Lr . B & Lp . B = ClosedProd (W,a1,b1) ) by A38, A2, A1;
A40: ( W preserves_No_Comparison_on ClosedProd (W,a1,b1) & W c= ClosedProd (W,a1,b1) ) by A38, A39, A1, A2;
then A41: W is almost-No-order by XBOOLE_1:1;

suppose ( a1 in a or ( a1 = a & b1 c= b ) ) ; :: thesis:

then ClosedProd (S,a1,b1) c= ClosedProd (S,a,b) by Th17;
then S preserves_No_Comparison_on ClosedProd (S,a1,b1) by A19;
then A42: S /\ (ClosedProd (S,a1,b1)) = W /\ (ClosedProd (W,a1,b1)) by A40, A20, A41, Th23;
[r,l] in W /\ (ClosedProd (W,a1,b1)) by A37, A38, A39, A40, XBOOLE_0:def 4;
hence contradiction by A36, A42, XBOOLE_0:def 4; :: thesis:

end;

suppose A43: ( not a1 in a & ( not a1 = a or not b1 c= b ) ) ; :: thesis:

then A44: a c= a1 by ORDINAL1:16;
( a in a1 or ( a = a1 & b c= b1 ) )

assume A45: ( not a in a1 & ( not a = a1 or not b c= b1 ) ) ; :: thesis:
then a1 c= a by ORDINAL1:16;
hence contradiction by A45, A43, A44, XBOOLE_0:def 10; :: thesis:

end;

then ClosedProd (W,a,b) c= ClosedProd (W,a1,b1) by Th17;
then W preserves_No_Comparison_on ClosedProd (W,a,b) by A40;
then S /\ (ClosedProd (S,a,b)) = W /\ (ClosedProd (W,a,b)) by A19, A20, A41, Th23;
then [x,y] in W /\ (ClosedProd (W,a,b)) by A16, A17, A18, A19, XBOOLE_0:def 4;
then [x,y] in W by XBOOLE_0:def 4;
then ( x <= W,y & [x,y] in ClosedProd (W,a1,b1) ) by A40;
then {x} << W, R_ y by A40;
then not l >= W,r by A35;
hence contradiction by A37, A38, A39; :: thesis:

end;

hence ( L_ x << R,{y} & {x} << R, R_ y ) by A22; :: thesis:

end;

assume A46: ( L_ x << R,{y} & {x} << R, R_ y ) ; :: thesis:
assume A47: not x <= R,y ; :: thesis:
A48: not x <= T,y

assume A49: x <= T,y ; :: thesis:
T in rng Lr by A13, A14, A1, FUNCT_1:def 3;
hence contradiction by A47, A49, A6, TARSKI:def 4; :: thesis:

end;

per cases by A48, A15, A12, A13;

suppose not L_ x << T,{y} ; :: thesis:

then consider l, r being object such that
A50: ( l in L_ x & r in {y} & l >= T,r ) ;
T in rng Lr by A13, A14, A1, FUNCT_1:def 3;
then r <= R,l by A50, A6, TARSKI:def 4;
hence contradiction by A46, A50; :: thesis:

end;

suppose not {x} << T, R_ y ; :: thesis:

then consider l, r being object such that
A51: ( l in {x} & r in R_ y & l >= T,r ) ;
T in rng Lr by A13, A14, A1, FUNCT_1:def 3;
then r <= R,l by A51, A6, TARSKI:def 4;
hence contradiction by A46, A51; :: thesis:

end;

hence ( R preserves_No_Comparison_on union (rng Lp) & R c= union (rng Lp) ) by A7; :: thesis:
let A, a, b be Ordinal; :: thesis:
let S be Relation; :: thesis:
assume A52: ( A in dom Lp & S = Lr . A & Lp . A = ClosedProd (S,a,b) ) ; :: thesis:
A53: R /\ [:(BeforeGames a),(BeforeGames a):] c= S /\ [:(BeforeGames a),(BeforeGames a):]

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A54: [x,y] in R /\ [:(BeforeGames a),(BeforeGames a):] ; :: thesis:
A55: [x,y] in [:(BeforeGames a),(BeforeGames a):] by A54, XBOOLE_0:def 4;
[x,y] in R by A54, XBOOLE_0:def 4;
then consider Y being set such that
A56: ( [x,y] in Y & Y in rng Lr ) by A6, TARSKI:def 4;
consider B being object such that
A57: ( B in dom Lr & Lr . B = Y ) by A56, FUNCT_1:def 3;
reconsider B = B as Ordinal by A57;
consider a1, b1 being Ordinal, W being Relation such that
A58: ( W = Lr . B & Lp . B = ClosedProd (W,a1,b1) ) by A57, A1, A2;
reconsider W = Lr . B as Relation by A57, A1, A2;
A59: ( S preserves_No_Comparison_on Lp . A & S c= Lp . A ) by A52, A2;
then A60: S is almost-No-order by A52, XBOOLE_1:1;
A61: ( W preserves_No_Comparison_on Lp . B & W c= Lp . B ) by A57, A1, A2;
then A62: W is almost-No-order by A58, XBOOLE_1:1;

suppose A63: ( not a1 in a & ( not a1 = a or not b1 c= b ) ) ; :: thesis:

then A64: a c= a1 by ORDINAL1:16;
( a in a1 or ( a = a1 & b c= b1 ) )

assume A65: ( not a in a1 & ( not a = a1 or not b c= b1 ) ) ; :: thesis:
then a1 c= a by ORDINAL1:16;
hence contradiction by A65, A63, A64, XBOOLE_0:def 10; :: thesis:

end;

then ClosedProd (W,a,b) c= ClosedProd (W,a1,b1) by Th17;
then W preserves_No_Comparison_on ClosedProd (W,a,b) by A61, A58;
then A66: S /\ (ClosedProd (S,a,b)) = W /\ (ClosedProd (W,a,b)) by A62, A60, A52, A59, Th23;
[x,y] in ClosedProd (W,a1,b1) by A56, A57, A61, A58;
then A67: ( x in Day (W,a1) & y in Day (W,a1) ) by ZFMISC_1:87;
A68: ( x in BeforeGames a & y in BeforeGames a ) by A55, ZFMISC_1:87;
then consider Ox being Ordinal such that
A69: ( Ox in a & x in Games Ox ) by Def5;
consider Oy being Ordinal such that
A70: ( Oy in a & y in Games Oy ) by A68, Def5;
A71: Day (W,Ox) c= Day (W,a) by Th9, A69, ORDINAL1:def 2;
A72: x in Day (W,Ox) by A67, A69, Th12;
then born (W,x) c= Ox by Def8;
then A73: ( born (W,x) in a & x in Day (W,a) ) by A69, A71, A72, ORDINAL1:12;
A74: Day (W,Oy) c= Day (W,a) by A70, ORDINAL1:def 2, Th9;
A75: y in Day (W,Oy) by A67, A70, Th12;
then born (W,y) c= Oy by Def8;
then ( born (W,y) in a & y in Day (W,a) ) by A70, A74, A75, ORDINAL1:12;
then [x,y] in ClosedProd (W,a,b) by A73, Def10;
then [x,y] in W /\ (ClosedProd (W,a,b)) by A56, A57, XBOOLE_0:def 4;
then [x,y] in S by A66, XBOOLE_0:def 4;
hence [x,y] in S /\ [:(BeforeGames a),(BeforeGames a):] by A55, XBOOLE_0:def 4; :: thesis:

end;

suppose ( a1 in a or ( a1 = a & b1 c= b ) ) ; :: thesis:

then ClosedProd (S,a1,b1) c= ClosedProd (S,a,b) by Th17;
then S preserves_No_Comparison_on ClosedProd (S,a1,b1) by A52, A59;
then A76: S /\ (ClosedProd (S,a1,b1)) = W /\ (ClosedProd (W,a1,b1)) by A61, A62, A60, A58, Th23;
[x,y] in W /\ (ClosedProd (W,a1,b1)) by A56, A57, A61, A58, XBOOLE_0:def 4;
then [x,y] in S by A76, XBOOLE_0:def 4;
hence [x,y] in S /\ [:(BeforeGames a),(BeforeGames a):] by A55, XBOOLE_0:def 4; :: thesis:

end;

S /\ [:(BeforeGames a),(BeforeGames a):] c= R /\ [:(BeforeGames a),(BeforeGames a):]

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A77: [x,y] in S /\ [:(BeforeGames a),(BeforeGames a):] ; :: thesis:
A78: [x,y] in [:(BeforeGames a),(BeforeGames a):] by A77, XBOOLE_0:def 4;
A79: [x,y] in S by A77, XBOOLE_0:def 4;
S in rng Lr by A52, A1, FUNCT_1:def 3;
then [x,y] in R by A79, A6, TARSKI:def 4;
hence [x,y] in R /\ [:(BeforeGames a),(BeforeGames a):] by A78, XBOOLE_0:def 4; :: thesis:

end;

hence R /\ [:(BeforeGames a),(BeforeGames a):] = S /\ [:(BeforeGames a),(BeforeGames a):] by A53, XBOOLE_0:def 10; :: thesis:

end;

theorem Th25: :: SURREAL0:25

for A, B being Ordinal
for R being Relation
for a, b being object holds
( [a,b] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) iff ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ) )

let A, B be Ordinal; :: thesis:
let R be Relation; :: thesis:
let a, b be object ; :: thesis:
thus ( [a,b] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) implies ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ) ) :: thesis:

assume A1: [a,b] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) ; :: thesis:
then A2: ( [a,b] in ClosedProd (R,A,B) & not [a,b] in OpenProd (R,A,B) ) by XBOOLE_0:def 5;
A3: ( a in Day (R,A) & b in Day (R,A) ) by ZFMISC_1:87, A1;

per cases by A2, Def10;

suppose ( born (R,a) in A & born (R,b) in A ) ; :: thesis:

hence ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ) by A2, A3, Def9; :: thesis:

end;

suppose A4: ( born (R,a) = A & born (R,b) c= B ) ; :: thesis:

then not born (R,b) in B by A2, A3, Def9;
then B c= born (R,b) by ORDINAL1:16;
hence ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ) by A1, ZFMISC_1:87, A4, XBOOLE_0:def 10; :: thesis:

end;

suppose A5: ( born (R,a) c= B & born (R,b) = A ) ; :: thesis:

then not born (R,a) in B by A2, A3, Def9;
then B c= born (R,a) by ORDINAL1:16;
hence ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ) by A1, ZFMISC_1:87, A5, XBOOLE_0:def 10; :: thesis:

end;

assume that
A6: ( a in Day (R,A) & b in Day (R,A) ) and
A7: ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ; :: thesis:
A8: not [a,b] in OpenProd (R,A,B)

assume [a,b] in OpenProd (R,A,B) ; :: thesis:
then ( ( born (R,a) in A & born (R,b) in A ) or ( born (R,a) = A & born (R,b) in B ) or ( born (R,a) in B & born (R,b) = A ) ) by A6, Def9;
hence contradiction by A7; :: thesis:

end;

[a,b] in ClosedProd (R,A,B) by A6, A7, Def10;
hence [a,b] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) by A8, XBOOLE_0:def 5; :: thesis:

end;

theorem Th26: :: SURREAL0:26

for A, B being Ordinal
for R being Relation st R preserves_No_Comparison_on OpenProd (R,A,B) & R c= OpenProd (R,A,B) holds
ex S being Relation st
( R c= S & S preserves_No_Comparison_on ClosedProd (S,A,B) & S c= ClosedProd (S,A,B) )

let A, B be Ordinal; :: thesis:
let R be Relation; :: thesis:
assume A1: ( R preserves_No_Comparison_on OpenProd (R,A,B) & R c= OpenProd (R,A,B) ) ; :: thesis:
set CC = { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ;
{ [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } is Relation-like

let z be object ; :: according to RELAT_1:def 1 :: thesis:
assume z in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ; :: thesis:
then ex x, y being Element of Day (R,A) st
( z = [x,y] & ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) ;
hence ex b₁, b₂ being object st z = [b₁,b₂] ; :: thesis:

end;

then reconsider RCC = R \/ { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } as Relation ;
take RCC ; :: thesis:
thus R c= RCC by XBOOLE_1:7; :: thesis:
A2: R /\ [:(BeforeGames A),(BeforeGames A):] c= RCC /\ [:(BeforeGames A),(BeforeGames A):] by XBOOLE_1:7, XBOOLE_1:26;
A3: RCC /\ [:(BeforeGames A),(BeforeGames A):] c= R /\ [:(BeforeGames A),(BeforeGames A):]

let y1, z1 be object ; :: according to RELAT_1:def 3 :: thesis:
assume [y1,z1] in RCC /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis:
then A4: ( [y1,z1] in RCC & [y1,z1] in [:(BeforeGames A),(BeforeGames A):] ) by XBOOLE_0:def 4;
not [y1,z1] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) }

assume [y1,z1] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ; :: thesis:
then consider y, z being Element of Day (R,A) such that
A5: [y1,z1] = [y,z] and
A6: ( ( born (R,y) = B & born (R,z) = A ) or ( born (R,y) = A & born (R,z) = B ) ) and
( L_ y << R,{z} & {y} << R, R_ z ) ;
A7: ( y in BeforeGames A & z in BeforeGames A ) by A5, A4, ZFMISC_1:87;
then consider Oy being Ordinal such that
A8: ( Oy in A & y in Games Oy ) by Def5;
y in Day (R,Oy) by A8, Th12;
then A9: born (R,y) c= Oy by Def8;
consider Oz being Ordinal such that
A10: ( Oz in A & z in Games Oz ) by A7, Def5;
z in Day (R,Oz) by A10, Th12;
then born (R,z) c= Oz by Def8;
hence contradiction by A6, A9, A8, ORDINAL1:12, A10; :: thesis:

end;

then [y1,z1] in R by A4, XBOOLE_0:def 3;
hence [y1,z1] in R /\ [:(BeforeGames A),(BeforeGames A):] by A4, XBOOLE_0:def 4; :: thesis:

end;

A11: RCC c= ClosedProd (R,A,B)

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A12: [x,y] in RCC ; :: thesis:

per cases by A12, XBOOLE_0:def 3;

suppose [x,y] in R ; :: thesis:

then ( [x,y] in OpenProd (R,A,B) & OpenProd (R,A,B) c= ClosedProd (R,A,B) ) by A1, Th16;
hence [x,y] in ClosedProd (R,A,B) ; :: thesis:

end;

suppose [x,y] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ; :: thesis:

then consider x1, y1 being Element of Day (R,A) such that
A13: [x,y] = [x1,y1] and
A14: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) ;
thus [x,y] in ClosedProd (R,A,B) by A13, A14, Def10; :: thesis:

end;

RCC preserves_No_Comparison_on ClosedProd (R,A,B)

let x, y be object ; :: according to SURREAL0:def 11 :: thesis:
assume A15: [x,y] in ClosedProd (R,A,B) ; :: thesis:
A16: ( x in Day (R,A) & y in Day (R,A) ) by A15, ZFMISC_1:87;

suppose A17: [x,y] in OpenProd (R,A,B) ; :: thesis:

thus ( x <= RCC,y implies ( L_ x << RCC,{y} & {x} << RCC, R_ y ) ) :: thesis:

assume x <= RCC,y ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose [x,y] in R ; :: thesis:

then x <= R,y ;
then A18: ( L_ x << R,{y} & {x} << R, R_ y ) by A1;
thus L_ x << RCC,{y} :: thesis:

given l, r being object such that A19: ( l in L_ x & r in {y} & l >= RCC,r ) ; :: according to SURREAL0:def 3 :: thesis:
A20: r = y by A19, TARSKI:def 1;
not l >= R,r by A19, A18;
then [r,l] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } by A19, XBOOLE_0:def 3;
then consider x1, y1 being Element of Day (R,A) such that
A21: [r,l] = [x1,y1] and
A22: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) ;
A23: ( x in Day (R,A) & y in Day (R,A) ) by A15, ZFMISC_1:87;
then A24: x in Day (R,(born (R,x))) by Def8;
l in (L_ x) \/ (R_ x) by A19, XBOOLE_0:def 3;
then consider Ol being Ordinal such that
A25: ( Ol in born (R,x) & l in Day (R,Ol) ) by A24, Th7;
A26: ( r = x1 & l = y1 ) by A21, XTUPLE_0:1;
A27: born (R,l) c= Ol by A25, Def8;
( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) by A17, A23, Def9;
hence contradiction by A27, A26, A25, A20, A22; :: thesis:

end;

thus {x} << RCC, R_ y :: thesis:

given l, r being object such that A28: ( l in {x} & r in R_ y & l >= RCC,r ) ; :: according to SURREAL0:def 3 :: thesis:
A29: l = x by A28, TARSKI:def 1;
not l >= R,r by A28, A18;
then [r,l] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } by A28, XBOOLE_0:def 3;
then consider x1, y1 being Element of Day (R,A) such that
A30: [r,l] = [x1,y1] and
A31: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) ;
A32: ( x in Day (R,A) & y in Day (R,A) ) by A15, ZFMISC_1:87;
then A33: y in Day (R,(born (R,y))) by Def8;
r in (L_ y) \/ (R_ y) by A28, XBOOLE_0:def 3;
then consider Or being Ordinal such that
A34: ( Or in born (R,y) & r in Day (R,Or) ) by A33, Th7;
A35: ( r = x1 & l = y1 ) by A30, XTUPLE_0:1;
A36: born (R,r) c= Or by A34, Def8;
( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) by A17, A32, Def9;
hence contradiction by A36, A31, A35, A29, A34; :: thesis:

end;

suppose [x,y] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ; :: thesis:

then consider x1, y1 being Element of Day (R,A) such that
A37: [x,y] = [x1,y1] and
A38: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) ;
( ( not born (R,x1) in B or not born (R,y1) = A ) & ( not born (R,x1) = A or not born (R,y1) in B ) & ( not born (R,x1) in A or not born (R,y1) in A ) ) by A38;
hence ( L_ x << RCC,{y} & {x} << RCC, R_ y ) by A37, A17, Def9; :: thesis:

end;

assume A39: ( L_ x << RCC,{y} & {x} << RCC, R_ y ) ; :: thesis:
A40: L_ x << R,{y}

given l, r being object such that A41: ( l in L_ x & r in {y} & l >= R,r ) ; :: according to SURREAL0:def 3 :: thesis:
l >= RCC,r by A41, XBOOLE_0:def 3;
hence contradiction by A39, A41; :: thesis:

end;

{x} << R, R_ y

given l, r being object such that A42: ( l in {x} & r in R_ y & l >= R,r ) ; :: according to SURREAL0:def 3 :: thesis:
l >= RCC,r by A42, XBOOLE_0:def 3;
hence contradiction by A39, A42; :: thesis:

end;

then x <= R,y by A17, A1, A40;
hence x <= RCC,y by XBOOLE_0:def 3; :: thesis:

end;

suppose A43: not [x,y] in OpenProd (R,A,B) ; :: thesis:

then [x,y] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) by A15, XBOOLE_0:def 5;
then A44: ( ( born (R,x) = A & born (R,y) = B ) or ( born (R,x) = B & born (R,y) = A ) ) by Th25;
thus ( x <= RCC,y implies ( L_ x << RCC,{y} & {x} << RCC, R_ y ) ) :: thesis:

assume x <= RCC,y ; :: thesis:
then ( [x,y] in R or [x,y] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } ) by XBOOLE_0:def 3;
then consider x1, y1 being Element of Day (R,A) such that
A45: [x,y] = [x1,y1] and
A46: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
A47: ( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) by A1, A43;
A48: ( x = x1 & y = y1 ) by A45, XTUPLE_0:1;
thus L_ x << RCC,{y} :: thesis:

given l, r being object such that A49: ( l in L_ x & r in {y} & l >= RCC,r ) ; :: according to SURREAL0:def 3 :: thesis:
A50: r = y by A49, TARSKI:def 1;
not l >= R,r by A49, A47, A48;
then [r,l] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } by A49, XBOOLE_0:def 3;
then consider x1, y1 being Element of Day (R,A) such that
A51: [r,l] = [x1,y1] and
A52: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) ;
A53: x in Day (R,(born (R,x))) by A16, Def8;
l in (L_ x) \/ (R_ x) by A49, XBOOLE_0:def 3;
then consider Ol being Ordinal such that
A54: ( Ol in born (R,x) & l in Day (R,Ol) ) by A53, Th7;
A55: ( r = x1 & l = y1 ) by A51, XTUPLE_0:1;
born (R,l) c= Ol by A54, Def8;
hence contradiction by A46, A48, A50, A52, A55, A54, ORDINAL1:12; :: thesis:

end;

thus {x} << RCC, R_ y :: thesis:

given l, r being object such that A56: ( l in {x} & r in R_ y & l >= RCC,r ) ; :: according to SURREAL0:def 3 :: thesis:
A57: l = x by A56, TARSKI:def 1;
not l >= R,r by A56, A47, A48;
then [r,l] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } by A56, XBOOLE_0:def 3;
then consider x1, y1 being Element of Day (R,A) such that
A58: [r,l] = [x1,y1] and
A59: ( ( born (R,x1) = B & born (R,y1) = A ) or ( born (R,x1) = A & born (R,y1) = B ) ) and
( L_ x1 << R,{y1} & {x1} << R, R_ y1 ) ;
A60: y in Day (R,(born (R,y))) by A16, Def8;
r in (L_ y) \/ (R_ y) by A56, XBOOLE_0:def 3;
then consider Or being Ordinal such that
A61: ( Or in born (R,y) & r in Day (R,Or) ) by A60, Th7;
A62: ( r = x1 & l = y1 ) by A58, XTUPLE_0:1;
born (R,r) c= Or by A61, Def8;
hence contradiction by A46, A48, A57, A59, A62, A61, ORDINAL1:12; :: thesis:

end;

assume A63: ( L_ x << RCC,{y} & {x} << RCC, R_ y ) ; :: thesis:
A64: L_ x << R,{y}

given l, r being object such that A65: ( l in L_ x & r in {y} & l >= R,r ) ; :: according to SURREAL0:def 3 :: thesis:
l >= RCC,r by A65, XBOOLE_0:def 3;
hence contradiction by A63, A65; :: thesis:

end;

{x} << R, R_ y

given l, r being object such that A66: ( l in {x} & r in R_ y & l >= R,r ) ; :: according to SURREAL0:def 3 :: thesis:
l >= RCC,r by A66, XBOOLE_0:def 3;
hence contradiction by A63, A66; :: thesis:

end;

then [x,y] in { [x,y] where x, y is Element of Day (R,A) : ( ( ( born (R,x) = B & born (R,y) = A ) or ( born (R,x) = A & born (R,y) = B ) ) & L_ x << R,{y} & {x} << R, R_ y ) } by A64, A44, A16;
hence x <= RCC,y by XBOOLE_0:def 3; :: thesis:

end;

hence ( RCC preserves_No_Comparison_on ClosedProd (RCC,A,B) & RCC c= ClosedProd (RCC,A,B) ) by A3, Th15, A2, XBOOLE_0:def 10, A11; :: thesis:

end;

theorem Th27: :: SURREAL0:27

for A, B being Ordinal st ex R being Relation st
( R preserves_No_Comparison_on OpenProd (R,A,{}) & R c= OpenProd (R,A,{}) ) holds
ex S being Relation st
( S preserves_No_Comparison_on ClosedProd (S,A,B) & S c= ClosedProd (S,A,B) )

let A, B be Ordinal; :: thesis:
assume A1: ex R being Relation st
( R preserves_No_Comparison_on OpenProd (R,A,{}) & R c= OpenProd (R,A,{}) ) ; :: thesis:
defpred S₁[ Ordinal] means ex R being Relation st
( R preserves_No_Comparison_on ClosedProd (R,A,$1) & R c= ClosedProd (R,A,$1) );
A2: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

let D be Ordinal; :: thesis:
assume A3: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:

suppose A4: D = {} ; :: thesis:

consider R being Relation such that
A5: ( R preserves_No_Comparison_on OpenProd (R,A,{}) & R c= OpenProd (R,A,{}) ) by A1;
ex S being Relation st
( R c= S & S preserves_No_Comparison_on ClosedProd (S,A,{}) & S c= ClosedProd (S,A,{}) ) by Th26, A5;
hence S₁[D] by A4; :: thesis:

end;

suppose A6: D <> {} ; :: thesis:

defpred S₂[ object , object ] means for B being Ordinal st B = $1 holds
ex R being Relation st
( $2 = R & R preserves_No_Comparison_on ClosedProd (R,A,B) & R c= ClosedProd (R,A,B) );
A7: for e being object st e in D holds
ex u being object st S₂[e,u]

let e be object ; :: thesis:
assume A8: e in D ; :: thesis:
reconsider E = e as Ordinal by A8;
consider R being Relation such that
A9: ( R preserves_No_Comparison_on ClosedProd (R,A,E) & R c= ClosedProd (R,A,E) ) by A3, A8;
take R ; :: thesis:
thus S₂[e,R] by A9; :: thesis:

end;

consider Lr being Function such that
A10: ( dom Lr = D & ( for e being object st e in D holds
S₂[e,Lr . e] ) ) from CLASSES1:sch 1(A7);
reconsider Lr = Lr as Sequence by A10, ORDINAL1:def 7;
defpred S₃[ object , object ] means for B being Ordinal
for R being Relation st B = $1 & R = Lr . B holds
$2 = ClosedProd (R,A,B);
A11: for e being object st e in D holds
ex u being object st S₃[e,u]

let e be object ; :: thesis:
assume A12: e in D ; :: thesis:
reconsider E = e as Ordinal by A12;
consider R being Relation such that
A13: ( Lr . E = R & R preserves_No_Comparison_on ClosedProd (R,A,E) & R c= ClosedProd (R,A,E) ) by A12, A10;
take ClosedProd (R,A,E) ; :: thesis:
thus S₃[e, ClosedProd (R,A,E)] by A13; :: thesis:

end;

consider Lp being Function such that
A14: ( dom Lp = D & ( for e being object st e in D holds
S₃[e,Lp . e] ) ) from CLASSES1:sch 1(A11);
reconsider Lp = Lp as Sequence by A14, ORDINAL1:def 7;
A15: for E being Ordinal st E in dom Lp holds
( ex a, b being Ordinal ex R being Relation st
( R = Lr . E & Lp . E = ClosedProd (R,a,b) ) & Lr . E is Relation & ( for R being Relation st R = Lr . E holds
( R preserves_No_Comparison_on Lp . E & R c= Lp . E ) ) )

let E be Ordinal; :: thesis:
assume A16: E in dom Lp ; :: thesis:
consider R being Relation such that
A17: ( Lr . E = R & R preserves_No_Comparison_on ClosedProd (R,A,E) & R c= ClosedProd (R,A,E) ) by A16, A10, A14;
thus ( ex a, b being Ordinal ex R being Relation st
( R = Lr . E & Lp . E = ClosedProd (R,a,b) ) & Lr . E is Relation & ( for R being Relation st R = Lr . E holds
( R preserves_No_Comparison_on Lp . E & R c= Lp . E ) ) ) by A17, A16, A14; :: thesis:

end;

then reconsider RR = union (rng Lr) as Relation by A14, A10, Th24;
A18: ( RR preserves_No_Comparison_on union (rng Lp) & RR c= union (rng Lp) ) by A15, A14, A10, Th24;
A19: union (rng Lp) c= OpenProd (RR,A,D)

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union (rng Lp) ; :: thesis:
then consider Y being set such that
A20: ( x in Y & Y in rng Lp ) by TARSKI:def 4;
consider E being object such that
A21: ( E in dom Lp & Y = Lp . E ) by A20, FUNCT_1:def 3;
reconsider E = E as Ordinal by A21;
reconsider R = Lr . E as Relation by A21, A15;
A22: Lp . E = ClosedProd (R,A,E) by A21, A14;
then RR /\ [:(BeforeGames A),(BeforeGames A):] = R /\ [:(BeforeGames A),(BeforeGames A):] by A15, A14, A10, Th24, A21;
then A23: x in ClosedProd (RR,A,E) by A20, A21, A22, Th15;
ClosedProd (RR,A,E) c= OpenProd (RR,A,D) by Th18, A21, A14;
hence x in OpenProd (RR,A,D) by A23; :: thesis:

end;

OpenProd (RR,A,D) c= union (rng Lp)

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A24: [x,y] in OpenProd (RR,A,D) ; :: thesis:
A25: ( x in Day (RR,A) & y in Day (RR,A) ) by A24, ZFMISC_1:87;

per cases by A24, Def9;

suppose A26: ( born (RR,x) in A & born (RR,y) in A ) ; :: thesis:

consider B being object such that
A27: B in D by A6, XBOOLE_0:def 1;
reconsider B = B as Ordinal by A27;
consider R being Relation such that
A28: ( Lr . B = R & R preserves_No_Comparison_on ClosedProd (R,A,B) & R c= ClosedProd (R,A,B) ) by A27, A10;
A29: Lp . B = ClosedProd (R,A,B) by A27, A28, A14;
then RR /\ [:(BeforeGames A),(BeforeGames A):] = R /\ [:(BeforeGames A),(BeforeGames A):] by A27, A28, A15, A14, A10, Th24;
then A30: ClosedProd (RR,A,B) = ClosedProd (R,A,B) by Th15;
A31: [x,y] in ClosedProd (RR,A,B) by A26, A25, Def10;
Lp . B in rng Lp by A27, A14, FUNCT_1:def 3;
hence [x,y] in union (rng Lp) by A30, A29, A31, TARSKI:def 4; :: thesis:

end;

suppose A32: ( born (RR,x) = A & born (RR,y) in D ) ; :: thesis:

set B = born (RR,y);
consider R being Relation such that
A33: ( Lr . (born (RR,y)) = R & R preserves_No_Comparison_on ClosedProd (R,A,(born (RR,y))) & R c= ClosedProd (R,A,(born (RR,y))) ) by A32, A10;
A34: Lp . (born (RR,y)) = ClosedProd (R,A,(born (RR,y))) by A33, A32, A14;
then RR /\ [:(BeforeGames A),(BeforeGames A):] = R /\ [:(BeforeGames A),(BeforeGames A):] by A32, A33, A15, A14, A10, Th24;
then A35: ClosedProd (RR,A,(born (RR,y))) = ClosedProd (R,A,(born (RR,y))) by Th15;
A36: [x,y] in ClosedProd (RR,A,(born (RR,y))) by A32, A25, Def10;
Lp . (born (RR,y)) in rng Lp by A32, A14, FUNCT_1:def 3;
hence [x,y] in union (rng Lp) by A35, A34, A36, TARSKI:def 4; :: thesis:

end;

suppose A37: ( born (RR,x) in D & born (RR,y) = A ) ; :: thesis:

set B = born (RR,x);
consider R being Relation such that
A38: ( Lr . (born (RR,x)) = R & R preserves_No_Comparison_on ClosedProd (R,A,(born (RR,x))) & R c= ClosedProd (R,A,(born (RR,x))) ) by A37, A10;
A39: Lp . (born (RR,x)) = ClosedProd (R,A,(born (RR,x))) by A38, A37, A14;
then RR /\ [:(BeforeGames A),(BeforeGames A):] = R /\ [:(BeforeGames A),(BeforeGames A):] by A37, A38, A15, A14, A10, Th24;
then A40: ClosedProd (RR,A,(born (RR,x))) = ClosedProd (R,A,(born (RR,x))) by Th15;
A41: [x,y] in ClosedProd (RR,A,(born (RR,x))) by A37, A25, Def10;
Lp . (born (RR,x)) in rng Lp by A37, A14, FUNCT_1:def 3;
hence [x,y] in union (rng Lp) by A40, A39, A41, TARSKI:def 4; :: thesis:

end;

then OpenProd (RR,A,D) = union (rng Lp) by A19, XBOOLE_0:def 10;
then ex R being Relation st
( RR c= R & R preserves_No_Comparison_on ClosedProd (R,A,D) & R c= ClosedProd (R,A,D) ) by A18, Th26;
hence S₁[D] ; :: thesis:

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A2);
hence ex S being Relation st
( S preserves_No_Comparison_on ClosedProd (S,A,B) & S c= ClosedProd (S,A,B) ) ; :: thesis:

end;

theorem Th28: :: SURREAL0:28

for A, B being Ordinal ex R being Relation st
( R preserves_No_Comparison_on ClosedProd (R,A,B) & R c= ClosedProd (R,A,B) )

let A, B be Ordinal; :: thesis:
defpred S₁[ Ordinal] means for B being Ordinal ex R being Relation st
( R preserves_No_Comparison_on ClosedProd (R,$1,B) & R c= ClosedProd (R,$1,B) );
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

let D be Ordinal; :: thesis:
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:
let B be Ordinal; :: thesis:
defpred S₂[ object , object ] means for B being Ordinal st B = $1 holds
ex R being Relation st
( $2 = R & R preserves_No_Comparison_on ClosedProd (R,B,B) & R c= ClosedProd (R,B,B) );
A3: for e being object st e in D holds
ex u being object st S₂[e,u]

let e be object ; :: thesis:
assume A4: e in D ; :: thesis:
reconsider E = e as Ordinal by A4;
consider R being Relation such that
A5: ( R preserves_No_Comparison_on ClosedProd (R,E,E) & R c= ClosedProd (R,E,E) ) by A4, A2;
take R ; :: thesis:
thus S₂[e,R] by A5; :: thesis:

end;

consider Lr being Function such that
A6: ( dom Lr = D & ( for e being object st e in D holds
S₂[e,Lr . e] ) ) from CLASSES1:sch 1(A3);
reconsider Lr = Lr as Sequence by A6, ORDINAL1:def 7;
defpred S₃[ object , object ] means for B being Ordinal
for R being Relation st B = $1 & R = Lr . B holds
$2 = ClosedProd (R,B,B);
A7: for e being object st e in D holds
ex u being object st S₃[e,u]

let e be object ; :: thesis:
assume A8: e in D ; :: thesis:
reconsider E = e as Ordinal by A8;
consider R being Relation such that
A9: ( Lr . E = R & R preserves_No_Comparison_on ClosedProd (R,E,E) & R c= ClosedProd (R,E,E) ) by A8, A6;
take ClosedProd (R,E,E) ; :: thesis:
thus S₃[e, ClosedProd (R,E,E)] by A9; :: thesis:

end;

consider Lp being Function such that
A10: ( dom Lp = D & ( for e being object st e in D holds
S₃[e,Lp . e] ) ) from CLASSES1:sch 1(A7);
reconsider Lp = Lp as Sequence by A10, ORDINAL1:def 7;
A11: for E being Ordinal st E in dom Lp holds
( ex a, b being Ordinal ex R being Relation st
( R = Lr . E & Lp . E = ClosedProd (R,a,b) ) & Lr . E is Relation & ( for R being Relation st R = Lr . E holds
( R preserves_No_Comparison_on Lp . E & R c= Lp . E ) ) )

let E be Ordinal; :: thesis:
assume A12: E in dom Lp ; :: thesis:
consider R being Relation such that
A13: ( Lr . E = R & R preserves_No_Comparison_on ClosedProd (R,E,E) & R c= ClosedProd (R,E,E) ) by A12, A6, A10;
thus ( ex a, b being Ordinal ex R being Relation st
( R = Lr . E & Lp . E = ClosedProd (R,a,b) ) & Lr . E is Relation & ( for R being Relation st R = Lr . E holds
( R preserves_No_Comparison_on Lp . E & R c= Lp . E ) ) ) by A13, A12, A10; :: thesis:

end;

then reconsider RR = union (rng Lr) as Relation by A10, A6, Th24;
A14: ( RR preserves_No_Comparison_on union (rng Lp) & RR c= union (rng Lp) ) by A11, A10, A6, Th24;
A15: union (rng Lp) c= OpenProd (RR,D,{})

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union (rng Lp) ; :: thesis:
then consider Y being set such that
A16: ( x in Y & Y in rng Lp ) by TARSKI:def 4;
consider E being object such that
A17: ( E in dom Lp & Y = Lp . E ) by A16, FUNCT_1:def 3;
reconsider E = E as Ordinal by A17;
A18: Day (RR,E) c= Day (RR,D) by A10, A17, Th9, ORDINAL1:def 2;
reconsider R = Lr . E as Relation by A17, A11;
A19: Lp . E = ClosedProd (R,E,E) by A17, A10;
then RR /\ [:(BeforeGames E),(BeforeGames E):] = R /\ [:(BeforeGames E),(BeforeGames E):] by A11, A10, A6, Th24, A17;
then A20: x in ClosedProd (RR,E,E) by A16, A17, A19, Th15;
then consider y, z being object such that
A21: ( y in Day (RR,E) & z in Day (RR,E) & [y,z] = x ) by ZFMISC_1:def 2;
( ( born (RR,y) in E & born (RR,z) in E ) or ( born (RR,y) = E & born (RR,z) c= E ) or ( born (RR,y) c= E & born (RR,z) = E ) ) by A20, A21, Def10;
then ( born (RR,y) in D & born (RR,z) in D ) by ORDINAL1:10, ORDINAL1:12, A10, A17;
hence x in OpenProd (RR,D,{}) by A18, A21, Def9; :: thesis:

end;

OpenProd (RR,D,{}) c= union (rng Lp)

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A22: [x,y] in OpenProd (RR,D,{}) ; :: thesis:
A23: ( x in Day (RR,D) & y in Day (RR,D) ) by A22, ZFMISC_1:87;
then A24: ( born (RR,x) in D & born (RR,y) in D ) by A22, Def9;

suppose A25: born (RR,x) c= born (RR,y) ; :: thesis:

set B = born (RR,y);
A26: Day (RR,(born (RR,x))) c= Day (RR,(born (RR,y))) by A25, Th9;
A27: ( x in Day (RR,(born (RR,x))) & y in Day (RR,(born (RR,y))) ) by A23, Def8;
consider R being Relation such that
A28: ( Lr . (born (RR,y)) = R & R preserves_No_Comparison_on ClosedProd (R,(born (RR,y)),(born (RR,y))) & R c= ClosedProd (R,(born (RR,y)),(born (RR,y))) ) by A24, A6;
A29: Lp . (born (RR,y)) = ClosedProd (R,(born (RR,y)),(born (RR,y))) by A24, A28, A10;
then RR /\ [:(BeforeGames (born (RR,y))),(BeforeGames (born (RR,y))):] = R /\ [:(BeforeGames (born (RR,y))),(BeforeGames (born (RR,y))):] by A24, A28, A11, A10, A6, Th24;
then A30: ClosedProd (RR,(born (RR,y)),(born (RR,y))) = ClosedProd (R,(born (RR,y)),(born (RR,y))) by Th15;
A31: [x,y] in ClosedProd (RR,(born (RR,y)),(born (RR,y))) by A25, Def10, A26, A27;
Lp . (born (RR,y)) in rng Lp by A24, A10, FUNCT_1:def 3;
hence [x,y] in union (rng Lp) by A30, A29, A31, TARSKI:def 4; :: thesis:

end;

suppose A32: not born (RR,x) c= born (RR,y) ; :: thesis:

set B = born (RR,x);
A33: Day (RR,(born (RR,y))) c= Day (RR,(born (RR,x))) by A32, Th9;
A34: ( y in Day (RR,(born (RR,y))) & x in Day (RR,(born (RR,x))) ) by A23, Def8;
consider R being Relation such that
A35: ( Lr . (born (RR,x)) = R & R preserves_No_Comparison_on ClosedProd (R,(born (RR,x)),(born (RR,x))) & R c= ClosedProd (R,(born (RR,x)),(born (RR,x))) ) by A24, A6;
A36: Lp . (born (RR,x)) = ClosedProd (R,(born (RR,x)),(born (RR,x))) by A24, A35, A10;
then RR /\ [:(BeforeGames (born (RR,x))),(BeforeGames (born (RR,x))):] = R /\ [:(BeforeGames (born (RR,x))),(BeforeGames (born (RR,x))):] by A24, A35, A11, A10, A6, Th24;
then A37: ClosedProd (RR,(born (RR,x)),(born (RR,x))) = ClosedProd (R,(born (RR,x)),(born (RR,x))) by Th15;
A38: [x,y] in ClosedProd (RR,(born (RR,x)),(born (RR,x))) by A32, A33, A34, Def10;
Lp . (born (RR,x)) in rng Lp by A24, A10, FUNCT_1:def 3;
hence [x,y] in union (rng Lp) by A37, A36, A38, TARSKI:def 4; :: thesis:

end;

then OpenProd (RR,D,{}) = union (rng Lp) by A15, XBOOLE_0:def 10;
hence ex R being Relation st
( R preserves_No_Comparison_on ClosedProd (R,D,B) & R c= ClosedProd (R,D,B) ) by A14, Th27; :: thesis:

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence ex R being Relation st
( R preserves_No_Comparison_on ClosedProd (R,A,B) & R c= ClosedProd (R,A,B) ) ; :: thesis:

end;

theorem Th29: :: SURREAL0:29

for A, B being Ordinal
for R being Relation st A in B holds
ClosedProd (R,A,A) = OpenProd (R,A,B)

let A, B be Ordinal; :: thesis:
let R be Relation; :: thesis:
assume A1: A in B ; :: thesis:
then A2: ClosedProd (R,A,A) c= ClosedProd (R,A,B) by Th17, ORDINAL1:def 2;
ClosedProd (R,A,B) c= ClosedProd (R,A,A)

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A3: [x,y] in ClosedProd (R,A,B) ; :: thesis:
A4: ( x in Day (R,A) & y in Day (R,A) ) by A3, ZFMISC_1:87;
then A5: ( born (R,x) c= A & born (R,y) c= A ) by Def8;
( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) by A4, A3, Def10;
hence [x,y] in ClosedProd (R,A,A) by A4, A5, Def10; :: thesis:

end;

then A6: ClosedProd (R,A,B) = ClosedProd (R,A,A) by A2, XBOOLE_0:def 10;
A7: ClosedProd (R,A,B) c= OpenProd (R,A,B) by A1, Th19;
OpenProd (R,A,B) c= ClosedProd (R,A,B) by Th16;
hence ClosedProd (R,A,A) = OpenProd (R,A,B) by A6, A7, XBOOLE_0:def 10; :: thesis:

end;

theorem Th30: :: SURREAL0:30

for A, B being Ordinal
for R being Relation st A c= B holds
ClosedProd (R,A,A) c= ClosedProd (R,B,B)

let A, B be Ordinal; :: thesis:
let R be Relation; :: thesis:
assume A c= B ; :: thesis:
then ( A = B or A in B ) by ORDINAL1:11, XBOOLE_0:def 8;
hence ClosedProd (R,A,A) c= ClosedProd (R,B,B) by Th17; :: thesis:

end;

Lm3: for A being Ordinal
for R being Relation holds ClosedProd (R,A,A) = [:(Day (R,A)),(Day (R,A)):]

let A be Ordinal; :: thesis:
let R be Relation; :: thesis:
let x, y be object ; :: according to RELAT_1:def 2 :: thesis:
thus ( [x,y] in ClosedProd (R,A,A) implies [x,y] in [:(Day (R,A)),(Day (R,A)):] ) ; :: thesis:
assume [x,y] in [:(Day (R,A)),(Day (R,A)):] ; :: thesis:
then A1: ( x in Day (R,A) & y in Day (R,A) ) by ZFMISC_1:87;
then A2: ( born (R,x) c= A & born (R,y) c= A ) by Def8;

suppose ( born (R,x) = A or born (R,y) = A ) ; :: thesis:

hence [x,y] in ClosedProd (R,A,A) by A1, A2, Def10; :: thesis:

end;

suppose ( born (R,x) <> A & born (R,y) <> A ) ; :: thesis:

then ( born (R,x) in A & born (R,y) in A ) by ORDINAL1:11, A2, XBOOLE_0:def 8;
hence [x,y] in ClosedProd (R,A,A) by A1, Def10; :: thesis:

end;

definition

let A be Ordinal;

func No_Ord A -> Relation means :Def12: :: SURREAL0:def 12
( it preserves_No_Comparison_on [:(Day (it,A)),(Day (it,A)):] & it c= [:(Day (it,A)),(Day (it,A)):] );

consider R being Relation such that
A1: ( R preserves_No_Comparison_on ClosedProd (R,A,A) & R c= ClosedProd (R,A,A) ) by Th28;
take R ; :: thesis:
thus ( R preserves_No_Comparison_on [:(Day (R,A)),(Day (R,A)):] & R c= [:(Day (R,A)),(Day (R,A)):] ) by A1, Lm3; :: thesis:

end;

let S1, S2 be Relation; :: thesis:
assume that
A2: ( S1 preserves_No_Comparison_on [:(Day (S1,A)),(Day (S1,A)):] & S1 c= [:(Day (S1,A)),(Day (S1,A)):] ) and
A3: ( S2 preserves_No_Comparison_on [:(Day (S2,A)),(Day (S2,A)):] & S2 c= [:(Day (S2,A)),(Day (S2,A)):] ) ; :: thesis:
A4: ( [:(Day (S1,A)),(Day (S1,A)):] = ClosedProd (S1,A,A) & [:(Day (S2,A)),(Day (S2,A)):] = ClosedProd (S2,A,A) ) by Lm3;
A5: ( S1 is almost-No-order & S2 is almost-No-order ) by A2, A3;
thus S1 = S1 /\ (ClosedProd (S1,A,A)) by A4, A2, XBOOLE_1:28
.= S2 /\ (ClosedProd (S2,A,A)) by A4, A5, A2, A3, Th23
.= S2 by A4, A3, XBOOLE_1:28 ; :: thesis:

end;

:: deftheorem Def12 defines No_Ord SURREAL0:def 12 :

registration

let A be Ordinal;

cluster No_Ord A -> almost-No-order ;

[:(Day ((No_Ord A),A)),(Day ((No_Ord A),A)):] = ClosedProd ((No_Ord A),A,A) by Lm3;
hence No_Ord A is almost-No-order by Def12; :: thesis:

end;

definition

let A be Ordinal;

func Day A -> non empty Subset of (Games A) equals :: SURREAL0:def 13
Day ((No_Ord A),A);

coherence ;

end;

:: deftheorem defines Day SURREAL0:def 13 :

definition

let o be object ;

attr o is surreal means :Def14: :: SURREAL0:def 14
ex A being Ordinal st o in Day A;

end;

:: deftheorem Def14 defines surreal SURREAL0:def 14 :

registration

cluster [{},{}] -> surreal ;

[{},{}] in Games 0 by Th2, TARSKI:def 1;
then [{},{}] in Day 0 by Th8;
hence [{},{}] is surreal ; :: thesis:

end;

cluster surreal for set ;

[{},{}] is surreal ;
hence ex b₁ being set st b₁ is surreal ; :: thesis:

end;

registration

let A be Ordinal;

cluster -> surreal for Element of Day A;

coherence ;

end;

definition

mode Surreal is surreal set ;

end;

definition

func 0_No -> Surreal equals :: SURREAL0:def 15
[{},{}];

coherence by TARSKI:1;

end;

:: deftheorem defines 0_No SURREAL0:def 15 :

registration

cluster surreal -> pair for set ;

let x be Surreal; :: thesis:
ex A being Ordinal st x in Day A by Def14;
hence x is pair ; :: thesis:

end;

registration

cluster surreal -> non empty for set ;

coherence ;

end;

definition

let X be set ;

attr X is surreal-membered means :Def16: :: SURREAL0:def 16
for o being object st o in X holds
o is surreal ;

end;

:: deftheorem Def16 defines surreal-membered SURREAL0:def 16 :

registration

cluster surreal-membered for set ;

take E = the empty set ; :: thesis:
thus E is surreal-membered ; :: thesis:

end;

registration

let x be Surreal;

cluster {x} -> surreal-membered ;

coherence by TARSKI:def 1;

cluster L_ x -> surreal-membered for set ;

consider A being Ordinal such that
A1: x in Day A by Def14;
let S be set ; :: thesis:
assume A2: S = L_ x ; :: thesis:
let y be object ; :: according to SURREAL0:def 16 :: thesis:
assume A3: y in S ; :: thesis:
y in (L_ x) \/ (R_ x) by A2, A3, XBOOLE_0:def 3;
then consider O being Ordinal such that
A4: ( O in A & y in Day ((No_Ord A),O) ) by A1, Th7;
( Day ((No_Ord A),O) c= Day ((No_Ord A),A) & Day ((No_Ord A),A) = Day A ) by Th9, A4, ORDINAL1:def 2;
hence y is surreal by A4; :: thesis:

end;

cluster R_ x -> surreal-membered for set ;

consider A being Ordinal such that
A5: x in Day A by Def14;
let S be set ; :: thesis:
assume A6: S = R_ x ; :: thesis:
let y be object ; :: according to SURREAL0:def 16 :: thesis:
assume A7: y in S ; :: thesis:
y in (L_ x) \/ (R_ x) by A6, A7, XBOOLE_0:def 3;
then consider O being Ordinal such that
A8: ( O in A & y in Day ((No_Ord A),O) ) by A5, Th7;
( Day ((No_Ord A),O) c= Day ((No_Ord A),A) & Day ((No_Ord A),A) = Day A ) by Th9, A8, ORDINAL1:def 2;
hence y is surreal by A8; :: thesis:

end;

registration

let X, Y be surreal-membered set ;

cluster X \/ Y -> surreal-membered ;

let o be object ; :: according to SURREAL0:def 16 :: thesis:
assume o in X \/ Y ; :: thesis:
then ( o in X or o in Y ) by XBOOLE_0:def 3;
hence o is surreal by Def16; :: thesis:

end;

cluster X \ Y -> surreal-membered ;

coherence by Def16;

cluster X /\ Y -> surreal-membered ;

let o be object ; :: according to SURREAL0:def 16 :: thesis:
assume o in X /\ Y ; :: thesis:
then o in X by XBOOLE_0:def 4;
hence o is surreal by Def16; :: thesis:

end;

registration

cluster non empty surreal-membered for set ;

take {0_No} ; :: thesis:
thus ( not {0_No} is empty & {0_No} is surreal-membered ) ; :: thesis:

end;

definition

let x, y be Surreal;

pred x <= y means :: SURREAL0:def 17
ex A being Ordinal st x <= No_Ord A,y;

end;

:: deftheorem defines <= SURREAL0:def 17 :

theorem Th31: :: SURREAL0:31

for A, B, X being Ordinal st X c= A & X c= B holds
(No_Ord A) /\ [:(BeforeGames X),(BeforeGames X):] = (No_Ord B) /\ [:(BeforeGames X),(BeforeGames X):]

let A, B, X be Ordinal; :: thesis:
assume A1: ( X c= A & X c= B ) ; :: thesis:
set SA = No_Ord A;
set SB = No_Ord B;
[:(Day ((No_Ord A),A)),(Day ((No_Ord A),A)):] = ClosedProd ((No_Ord A),A,A) by Lm3;
then A2: No_Ord A preserves_No_Comparison_on ClosedProd ((No_Ord A),A,A) by Def12;
( A c= X or X in A ) by ORDINAL1:16;
then ( X = A or X in A ) by A1, XBOOLE_0:def 10;
then ClosedProd ((No_Ord A),X,X) c= ClosedProd ((No_Ord A),A,A) by Th17;
then A3: No_Ord A preserves_No_Comparison_on ClosedProd ((No_Ord A),X,X) by A2;
[:(Day ((No_Ord B),B)),(Day ((No_Ord B),B)):] = ClosedProd ((No_Ord B),B,B) by Lm3;
then A4: No_Ord B preserves_No_Comparison_on ClosedProd ((No_Ord B),B,B) by Def12;
( B c= X or X in B ) by ORDINAL1:16;
then ( X = B or X in B ) by A1, XBOOLE_0:def 10;
then ClosedProd ((No_Ord B),X,X) c= ClosedProd ((No_Ord B),B,B) by Th17;
then No_Ord B preserves_No_Comparison_on ClosedProd ((No_Ord B),X,X) by A4;
then A5: (No_Ord A) /\ (ClosedProd ((No_Ord A),X,X)) = (No_Ord B) /\ (ClosedProd ((No_Ord B),X,X)) by Th23, A3;
( ClosedProd ((No_Ord A),X,X) = OpenProd ((No_Ord A),X,(succ X)) & ClosedProd ((No_Ord B),X,X) = OpenProd ((No_Ord B),X,(succ X)) ) by ORDINAL1:6, Th29;
hence (No_Ord A) /\ [:(BeforeGames X),(BeforeGames X):] = (No_Ord B) /\ [:(BeforeGames X),(BeforeGames X):] by A5, Th20; :: thesis:

end;

theorem Th32: :: SURREAL0:32

for A, B being Ordinal st A c= B holds
ClosedProd ((No_Ord A),A,A) = ClosedProd ((No_Ord B),A,A)

let A, B be Ordinal; :: thesis:
assume A c= B ; :: thesis:
then (No_Ord A) /\ [:(BeforeGames A),(BeforeGames A):] = (No_Ord B) /\ [:(BeforeGames A),(BeforeGames A):] by Th31;
hence ClosedProd ((No_Ord A),A,A) = ClosedProd ((No_Ord B),A,A) by Th15; :: thesis:

end;

theorem Th33: :: SURREAL0:33

for A being Ordinal
for a, b being object holds
( [a,b] in ClosedProd ((No_Ord A),A,A) iff ( a in Day A & b in Day A ) )

let A be Ordinal; :: thesis:
let a, b be object ; :: thesis:
thus ( [a,b] in ClosedProd ((No_Ord A),A,A) implies ( a in Day A & b in Day A ) ) by ZFMISC_1:87; :: thesis:
assume A1: ( a in Day A & b in Day A ) ; :: thesis:
then ( born ((No_Ord A),a) c= A & born ((No_Ord A),b) c= A ) by Def8;
then ( ( born ((No_Ord A),a) in A & born ((No_Ord A),b) in A ) or ( born ((No_Ord A),a) = A & born ((No_Ord A),b) c= A ) or ( born ((No_Ord A),a) c= A & born ((No_Ord A),b) = A ) or ( born ((No_Ord A),a) = A & born ((No_Ord A),b) = A ) ) by ORDINAL1:11, XBOOLE_0:def 8;
hence [a,b] in ClosedProd ((No_Ord A),A,A) by Def10, A1; :: thesis:

end;

theorem Th34: :: SURREAL0:34

for A, B being Ordinal st A c= B holds
No_Ord A = (No_Ord B) /\ (ClosedProd ((No_Ord B),A,A))

let A, B be Ordinal; :: thesis:
set R = No_Ord A;
set S = No_Ord B;
assume A c= B ; :: thesis:
then A1: ClosedProd ((No_Ord B),A,A) c= ClosedProd ((No_Ord B),B,B) by Th30;
A2: ( [:(Day ((No_Ord B),B)),(Day ((No_Ord B),B)):] = ClosedProd ((No_Ord B),B,B) & [:(Day ((No_Ord A),A)),(Day ((No_Ord A),A)):] = ClosedProd ((No_Ord A),A,A) ) by Lm3;
then No_Ord B preserves_No_Comparison_on ClosedProd ((No_Ord B),B,B) by Def12;
then ( No_Ord A preserves_No_Comparison_on ClosedProd ((No_Ord A),A,A) & No_Ord B preserves_No_Comparison_on ClosedProd ((No_Ord B),A,A) ) by A2, A1, Def12;
then A3: (No_Ord A) /\ (ClosedProd ((No_Ord A),A,A)) = (No_Ord B) /\ (ClosedProd ((No_Ord B),A,A)) by Th23;
No_Ord A c= ClosedProd ((No_Ord A),A,A) by A2, Def12;
hence No_Ord A = (No_Ord B) /\ (ClosedProd ((No_Ord B),A,A)) by A3, XBOOLE_1:28; :: thesis:

end;

theorem Th35: :: SURREAL0:35

for A, B being Ordinal st A c= B holds
Day A c= Day B

let A, B be Ordinal; :: thesis:
assume A1: A c= B ; :: thesis:
set R = No_Ord A;
set S = No_Ord B;
(No_Ord A) /\ [:(BeforeGames A),(BeforeGames A):] = (No_Ord B) /\ [:(BeforeGames A),(BeforeGames A):] by A1, Th31;
then Day ((No_Ord A),A) = Day ((No_Ord B),A) by Th10;
hence Day A c= Day B by A1, Th9; :: thesis:

end;

theorem Th36: :: SURREAL0:36

for A, B being Ordinal
for o being object st o in Day ((No_Ord A),B) & B c= A holds
o in Day B

let A, B be Ordinal; :: thesis:
let o be object ; :: thesis:
assume A1: ( o in Day ((No_Ord A),B) & B c= A ) ; :: thesis:
then (No_Ord A) /\ [:(BeforeGames B),(BeforeGames B):] = (No_Ord B) /\ [:(BeforeGames B),(BeforeGames B):] by Th31;
hence o in Day B by A1, Th10; :: thesis:

end;

definition

let x be Surreal;

func born x -> Ordinal means :Def18: :: SURREAL0:def 18
( x in Day it & ( for O being Ordinal st x in Day O holds
it c= O ) );

consider O being Ordinal such that
A1: x in Day O by Def14;
take b = born ((No_Ord O),x); :: thesis:
A2: b c= O by A1, Def8;
A3: x in Day ((No_Ord O),b) by Def8, A1;
hence x in Day b by A2, Th36; :: thesis:
let A be Ordinal; :: thesis:
assume A4: x in Day A ; :: thesis:
(No_Ord b) /\ [:(BeforeGames b),(BeforeGames b):] = (No_Ord O) /\ [:(BeforeGames b),(BeforeGames b):] by A2, Th31;
then A5: b = born ((No_Ord b),x) by A3, Th11;
A6: born ((No_Ord A),x) c= A by A4, Def8;
assume A7: not b c= A ; :: thesis:
then (No_Ord b) /\ [:(BeforeGames A),(BeforeGames A):] = (No_Ord A) /\ [:(BeforeGames A),(BeforeGames A):] by Th31;
hence contradiction by A5, A7, A6, Th11, A4; :: thesis:

end;

let b1, b2 be Ordinal; :: thesis:
assume that
A8: ( x in Day b1 & ( for O being Ordinal st x in Day O holds
b1 c= O ) ) and
A9: ( x in Day b2 & ( for O being Ordinal st x in Day O holds
b2 c= O ) ) ; :: thesis:
( b1 c= b2 & b2 c= b1 ) by A8, A9;
hence b1 = b2 by XBOOLE_0:def 10; :: thesis:

end;

:: deftheorem Def18 defines born SURREAL0:def 18 :

theorem :: SURREAL0:37

for x being Surreal holds
( born x = {} iff x = 0_No )

let x be Surreal; :: thesis:

hereby :: thesis:

assume born x = {} ; :: thesis:
then x in Day {} by Def18;
hence x = 0_No by Th2, TARSKI:def 1; :: thesis:

end;

assume x = 0_No ; :: thesis:
then x in Games {} by Th2, TARSKI:def 1;
then x in Day {} by Th8;
then born x c= {} by Def18;
hence born x = {} ; :: thesis:

end;

theorem :: SURREAL0:38

for A being Ordinal
for x being Surreal st x in Day A holds
born x = born ((No_Ord A),x)

let A be Ordinal; :: thesis:
let x be Surreal; :: thesis:
set bx = born x;
set bS = born ((No_Ord A),x);
assume A1: x in Day A ; :: thesis:
then A2: x in Day ((No_Ord A),(born ((No_Ord A),x))) by Def8;
born ((No_Ord A),x) c= A by A1, Def8;
then x in Day (born ((No_Ord A),x)) by Th36, A2;
then A3: born x c= born ((No_Ord A),x) by Def18;
born x c= A by Def18, A1;
then A4: (No_Ord (born x)) /\ [:(BeforeGames (born x)),(BeforeGames (born x)):] = (No_Ord A) /\ [:(BeforeGames (born x)),(BeforeGames (born x)):] by Th31;
A5: x in Day (born x) by Def18;
then born ((No_Ord (born x)),x) = born ((No_Ord A),x) by A4, Th11;
then born ((No_Ord A),x) c= born x by A5, Def8;
hence born x = born ((No_Ord A),x) by A3, XBOOLE_0:def 10; :: thesis:

end;

theorem Th39: :: SURREAL0:39

for A, B being Ordinal
for a, b being object st a <= No_Ord A,b & a in Day B & b in Day B holds
a <= No_Ord B,b

let A, B be Ordinal; :: thesis:
let a, b be object ; :: thesis:
set R = No_Ord A;
set S = No_Ord B;
assume A1: ( a <= No_Ord A,b & a in Day B & b in Day B ) ; :: thesis:
then A2: [a,b] in ClosedProd ((No_Ord B),B,B) by Th33;

suppose A3: B c= A ; :: thesis:

then ClosedProd ((No_Ord B),B,B) = ClosedProd ((No_Ord A),B,B) by Th32;
then No_Ord B = (No_Ord A) /\ (ClosedProd ((No_Ord B),B,B)) by A3, Th34;
hence a <= No_Ord B,b by A1, A2, XBOOLE_0:def 4; :: thesis:

end;

suppose A c= B ; :: thesis:

end;

theorem Th40: :: SURREAL0:40

for x, y being Surreal holds
( x <= y iff for A being Ordinal st x in Day A & y in Day A holds
x <= No_Ord A,y )

let x, y be Surreal; :: thesis:
consider Ax being Ordinal such that
A1: x in Day Ax by Def14;
consider Ay being Ordinal such that
A2: y in Day Ay by Def14;
thus ( x <= y implies for A being Ordinal st x in Day A & y in Day A holds
x <= No_Ord A,y ) by Th39; :: thesis:
assume A3: for A being Ordinal st x in Day A & y in Day A holds
x <= No_Ord A,y ; :: thesis:
set A = Ax \/ Ay;
( Day Ax c= Day (Ax \/ Ay) & Day Ay c= Day (Ax \/ Ay) ) by Th35, XBOOLE_1:7;
hence x <= y by A1, A2, A3; :: thesis:

end;

definition

let L, R be set ;

pred L >>= R means :: SURREAL0:def 19
for l, r being Surreal st l in L & r in R holds
r <= l;

end;

:: deftheorem defines >>= SURREAL0:def 19 :

notation

let R, L be set ;
synonym L <<= R for R >>= L;

end;

definition

let L, R be set ;

pred L << R means :: SURREAL0:def 20
for l, r being Surreal st l in L & r in R holds
not r <= l;

end;

:: deftheorem defines << SURREAL0:def 20 :

notation

let L, R be set ;
synonym R >> L for L << R;

end;

theorem :: SURREAL0:41

for X1, X2, Y being set st X1 << Y & X2 << Y holds
X1 \/ X2 << Y

let X1, X2, Y be set ; :: thesis:
assume A1: ( X1 << Y & X2 << Y ) ; :: thesis:
let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A2: ( l in X1 \/ X2 & r in Y ) ; :: thesis:
( l in X1 or l in X2 ) by A2, XBOOLE_0:def 3;
hence not r <= l by A1, A2; :: thesis:

end;

theorem :: SURREAL0:42

for X, Y1, Y2 being set st X << Y1 & X << Y2 holds
X << Y1 \/ Y2

let X, Y1, Y2 be set ; :: thesis:
assume A1: ( X << Y1 & X << Y2 ) ; :: thesis:
let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A2: ( l in X & r in Y1 \/ Y2 ) ; :: thesis:
( r in Y1 or r in Y2 ) by A2, XBOOLE_0:def 3;
hence not r <= l by A1, A2; :: thesis:

end;

theorem Th43: :: SURREAL0:43

for x, y being Surreal holds
( x <= y iff ( L_ x << {y} & {x} << R_ y ) )

let x, y be Surreal; :: thesis:
consider Ax being Ordinal such that
A1: x in Day Ax by Def14;
consider Ay being Ordinal such that
A2: y in Day Ay by Def14;
set A = Ax \/ Ay;
A3: ( Day Ax c= Day (Ax \/ Ay) & Day Ay c= Day (Ax \/ Ay) ) by XBOOLE_1:7, Th35;
then A4: ( x in Day (Ax \/ Ay) & y in Day (Ax \/ Ay) ) by A1, A2;
set S = No_Ord (Ax \/ Ay);
[:(Day ((No_Ord (Ax \/ Ay)),(Ax \/ Ay))),(Day ((No_Ord (Ax \/ Ay)),(Ax \/ Ay))):] = ClosedProd ((No_Ord (Ax \/ Ay)),(Ax \/ Ay),(Ax \/ Ay)) by Lm3;
then A5: ( No_Ord (Ax \/ Ay) preserves_No_Comparison_on ClosedProd ((No_Ord (Ax \/ Ay)),(Ax \/ Ay),(Ax \/ Ay)) & No_Ord (Ax \/ Ay) c= ClosedProd ((No_Ord (Ax \/ Ay)),(Ax \/ Ay),(Ax \/ Ay)) ) by Def12;
thus ( x <= y implies ( L_ x << {y} & {x} << R_ y ) ) :: thesis:

assume x <= y ; :: thesis:
then x <= No_Ord (Ax \/ Ay),y by A3, A1, A2, Th40;
then A6: ( L_ x << No_Ord (Ax \/ Ay),{y} & {x} << No_Ord (Ax \/ Ay), R_ y ) by A5;
thus L_ x << {y} :: thesis:

given l, r being Surreal such that A7: ( l in L_ x & r in {y} & r <= l ) ; :: according to SURREAL0:def 20 :: thesis:
A8: r = y by A7, TARSKI:def 1;
l in (L_ x) \/ (R_ x) by A7, XBOOLE_0:def 3;
then consider Ol being Ordinal such that
A9: ( Ol in Ax \/ Ay & l in Day ((No_Ord (Ax \/ Ay)),Ol) ) by A4, Th7;
Day ((No_Ord (Ax \/ Ay)),Ol) c= Day ((No_Ord (Ax \/ Ay)),(Ax \/ Ay)) by Th9, A9, ORDINAL1:def 2;
hence contradiction by A9, A6, A3, A2, A8, A7, Th40; :: thesis:

end;

thus {x} << R_ y :: thesis:

given l, r being Surreal such that A10: ( l in {x} & r in R_ y & r <= l ) ; :: according to SURREAL0:def 20 :: thesis:
A11: l = x by A10, TARSKI:def 1;
r in (L_ y) \/ (R_ y) by A10, XBOOLE_0:def 3;
then consider Or being Ordinal such that
A12: ( Or in Ax \/ Ay & r in Day ((No_Ord (Ax \/ Ay)),Or) ) by A4, Th7;
Day ((No_Ord (Ax \/ Ay)),Or) c= Day ((No_Ord (Ax \/ Ay)),(Ax \/ Ay)) by Th9, A12, ORDINAL1:def 2;
hence contradiction by A3, A12, A6, A1, A11, A10, Th40; :: thesis:

end;

assume A13: ( L_ x << {y} & {x} << R_ y ) ; :: thesis:
A14: [x,y] in ClosedProd ((No_Ord (Ax \/ Ay)),(Ax \/ Ay),(Ax \/ Ay)) by A3, A1, A2, Th33;
A15: L_ x << No_Ord (Ax \/ Ay),{y}

given l, r being object such that A16: ( l in L_ x & r in {y} & l >= No_Ord (Ax \/ Ay),r ) ; :: according to SURREAL0:def 3 :: thesis:
[r,l] in ClosedProd ((No_Ord (Ax \/ Ay)),(Ax \/ Ay),(Ax \/ Ay)) by A16, A5;
then ( l in Day (Ax \/ Ay) & r in Day (Ax \/ Ay) ) by ZFMISC_1:87;
then reconsider l = l, r = r as Surreal ;
r <= l by A16;
hence contradiction by A13, A16; :: thesis:

end;

{x} << No_Ord (Ax \/ Ay), R_ y

given l, r being object such that A17: ( l in {x} & r in R_ y & l >= No_Ord (Ax \/ Ay),r ) ; :: according to SURREAL0:def 3 :: thesis:
[r,l] in ClosedProd ((No_Ord (Ax \/ Ay)),(Ax \/ Ay),(Ax \/ Ay)) by A17, A5;
then ( l in Day (Ax \/ Ay) & r in Day (Ax \/ Ay) ) by ZFMISC_1:87;
then reconsider l = l, r = r as Surreal ;
r <= l by A17;
hence contradiction by A13, A17; :: thesis:

end;

then x <= No_Ord (Ax \/ Ay),y by A15, A14, A5;
hence x <= y ; :: thesis:

end;

theorem :: SURREAL0:44

for x, y being Surreal
for X1, X2, Y1, Y2 being set st ( for x being Surreal st x in X1 holds
ex y being Surreal st
( y in X2 & x <= y ) ) & ( for x being Surreal st x in Y2 holds
ex y being Surreal st
( y in Y1 & y <= x ) ) & x = [X1,Y1] & y = [X2,Y2] holds
x <= y

let x, y be Surreal; :: thesis:
let X1, X2, Y1, Y2 be set ; :: thesis:
assume A1: ( ( for x being Surreal st x in X1 holds
ex y being Surreal st
( y in X2 & x <= y ) ) & ( for x being Surreal st x in Y2 holds
ex y being Surreal st
( y in Y1 & y <= x ) ) & x = [X1,Y1] & y = [X2,Y2] ) ; :: thesis:
A2: L_ x << {y}

assume not L_ x << {y} ; :: thesis:
then consider l, r being Surreal such that
A3: ( l in L_ x & r in {y} & r <= l ) ;
consider z being Surreal such that
A4: ( z in L_ y & l <= z ) by A3, A1;
r = y by A3, TARSKI:def 1;
then ( L_ y << {l} & l in {l} ) by TARSKI:def 1, A3, Th43;
hence contradiction by A4; :: thesis:

end;

{x} << R_ y

assume not {x} << R_ y ; :: thesis:
then consider l, r being Surreal such that
A5: ( l in {x} & r in R_ y & r <= l ) ;
consider z being Surreal such that
A6: z in R_ x and
A7: z <= r by A5, A1;
l = x by TARSKI:def 1, A5;
then ( r in {r} & {r} << R_ x ) by TARSKI:def 1, A5, Th43;
hence contradiction by A6, A7; :: thesis:

end;

hence x <= y by A2, Th43; :: thesis:

end;

theorem Th45: :: SURREAL0:45

for x being Surreal holds L_ x << R_ x

let x be Surreal; :: thesis:
let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A1: ( l in L_ x & r in R_ x ) ; :: thesis:
consider A being Ordinal such that
A2: x in Day A by Def14;
set S = No_Ord A;
A3: L_ x << No_Ord A, R_ x by A2, Th7;
l in (L_ x) \/ (R_ x) by A1, XBOOLE_0:def 3;
then consider OL being Ordinal such that
A4: ( OL in A & l in Day ((No_Ord A),OL) ) by A2, Th7;
OL c= A by A4, ORDINAL1:def 2;
then A5: ( l in Day OL & Day OL c= Day A ) by A4, Th35, Th36;
r in (L_ x) \/ (R_ x) by A1, XBOOLE_0:def 3;
then consider OR being Ordinal such that
A6: ( OR in A & r in Day ((No_Ord A),OR) ) by A2, Th7;
OR c= A by A6, ORDINAL1:def 2;
then ( r in Day OR & Day OR c= Day A ) by A6, Th35, Th36;
hence not r <= l by A3, A1, A5, Th40; :: thesis:

end;

theorem :: SURREAL0:46

for X, Y being set
for A being Ordinal holds
( [X,Y] in Day A iff ( X << Y & ( for o being object st o in X \/ Y holds
ex O being Ordinal st
( O in A & o in Day O ) ) ) )

let X, Y be set ; :: thesis:
let A be Ordinal; :: thesis:
set S = No_Ord A;
thus ( [X,Y] in Day A implies ( X << Y & ( for x being object st x in X \/ Y holds
ex O being Ordinal st
( O in A & x in Day O ) ) ) ) :: thesis:

assume A1: [X,Y] in Day A ; :: thesis:
then reconsider XY = [X,Y] as Surreal ;
L_ XY << R_ XY by Th45;
hence X << Y ; :: thesis:
let x be object ; :: thesis:
assume x in X \/ Y ; :: thesis:
then x in (L_ XY) \/ (R_ XY) ;
then consider OL being Ordinal such that
A2: ( OL in A & x in Day ((No_Ord A),OL) ) by A1, Th7;
take OL ; :: thesis:
OL c= A by A2, ORDINAL1:def 2;
hence ( OL in A & x in Day OL ) by A2, Th36; :: thesis:

end;

set XY = [X,Y];
assume A3: ( X << Y & ( for x being object st x in X \/ Y holds
ex O being Ordinal st
( O in A & x in Day O ) ) ) ; :: thesis:
for x being object st x in (L_ [X,Y]) \/ (R_ [X,Y]) holds
ex O being Ordinal st
( O in A & x in Games O )

let x be object ; :: thesis:
assume x in (L_ [X,Y]) \/ (R_ [X,Y]) ; :: thesis:
then ex O being Ordinal st
( O in A & x in Day O ) by A3;
hence ex O being Ordinal st
( O in A & x in Games O ) ; :: thesis:

end;

then reconsider XY = [X,Y] as Element of Games A by Th4;
A4: L_ XY << No_Ord A, R_ XY

let l, r be object ; :: according to SURREAL0:def 3 :: thesis:
assume A5: ( l in L_ XY & r in R_ XY ) ; :: thesis:
assume A6: l >= No_Ord A,r ; :: thesis:
then ( [r,l] in No_Ord A & No_Ord A c= [:(Day ((No_Ord A),A)),(Day ((No_Ord A),A)):] & [:(Day ((No_Ord A),A)),(Day ((No_Ord A),A)):] = ClosedProd ((No_Ord A),A,A) ) by Def12, Lm3;
then ( r in Day A & l in Day A ) by Th33;
then reconsider r = r, l = l as Surreal ;
r <= l by A6;
hence contradiction by A3, A5; :: thesis:

end;

for x being object st x in (L_ XY) \/ (R_ XY) holds
ex O being Ordinal st
( O in A & x in Day ((No_Ord A),O) )

let x be object ; :: thesis:
assume x in (L_ XY) \/ (R_ XY) ; :: thesis:
then consider O being Ordinal such that
A7: ( O in A & x in Day O ) by A3;
O c= A by A7, ORDINAL1:def 2;
then (No_Ord A) /\ [:(BeforeGames O),(BeforeGames O):] = (No_Ord O) /\ [:(BeforeGames O),(BeforeGames O):] by Th31;
then Day ((No_Ord O),O) = Day ((No_Ord A),O) by Th10;
hence ex O being Ordinal st
( O in A & x in Day ((No_Ord A),O) ) by A7; :: thesis:

end;

hence [X,Y] in Day A by Th7, A4; :: thesis:

end;

theorem :: SURREAL0:47

for X being set st X is surreal-membered holds
ex M being Ordinal st
for o being object st o in X holds
ex A being Ordinal st
( A in M & o in Day A )

let X be set ; :: thesis:
assume A1: X is surreal-membered ; :: thesis:
defpred S₁[ object , object ] means ( $1 is Surreal & ( for z being Surreal st z = $1 holds
$2 = born z ) );
A2: for x, y, z being object st S₁[x,y] & S₁[x,z] holds
y = z

let x, y, z be object ; :: thesis:
assume A3: ( S₁[x,y] & S₁[x,z] ) ; :: thesis:
reconsider x = x as Surreal by A3;
thus y = born x by A3
.= z by A3 ; :: thesis:

end;

consider OO being set such that
A4: for z being object holds
( z in OO iff ex y being object st
( y in X & S₁[y,z] ) ) from TARSKI_0:sch 1(A2);
for x being set st x in OO holds
x is ordinal