let X, Y be set ; :: thesis: 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 A be Ordinal; :: thesis: ( [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 ) ) ) )
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: ( X << Y & ( for o being object st o in X \/ Y holds
ex O being Ordinal st
( O in A & o in Day O ) ) implies [X,Y] in Day A )

proof

assume A1: [X,Y] in Day A ; :: thesis: ( X << Y & ( for x being object st x in X \/ Y holds
ex O being Ordinal st
( O in A & x in Day O ) ) )
then reconsider XY = [X,Y] as Surreal ;
L_ XY << R_ XY by Th45;
hence X << Y ; :: thesis: for x being object st x in X \/ Y holds
ex O being Ordinal st
( O in A & x in Day O )
let x be object ; :: thesis: ( x in X \/ Y implies ex O being Ordinal st
( O in A & x in Day O ) )
assume x in X \/ Y ; :: thesis: ex O being Ordinal st
( O in A & x in Day O )
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 in A & x in Day OL )
OL c= A by A2, ORDINAL1:def 2;
hence ( OL in A & x in Day OL ) by A2, Th36; :: thesis: verum

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: [X,Y] in Day A
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 )

proof

let x be object ; :: thesis: ( x in (L_ [X,Y]) \/ (R_ [X,Y]) implies ex O being Ordinal st
( O in A & x in Games O ) )
assume x in (L_ [X,Y]) \/ (R_ [X,Y]) ; :: thesis: ex O being Ordinal st
( O in A & x in Games O )
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: verum

end;

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

proof

let l, r be object ; :: according to SURREAL0:def 3 :: thesis: ( l in L_ XY & r in R_ XY implies not l >= No_Ord A,r )
assume A5: ( l in L_ XY & r in R_ XY ) ; :: thesis: not l >= No_Ord A,r
assume A6: l >= No_Ord A,r ; :: thesis: contradiction
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: verum

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) )

proof

let x be object ; :: thesis: ( x in (L_ XY) \/ (R_ XY) implies ex O being Ordinal st
( O in A & x in Day ((No_Ord A),O) ) )
assume x in (L_ XY) \/ (R_ XY) ; :: thesis: ex O being Ordinal st
( O in A & x in Day ((No_Ord A),O) )
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: verum

end;

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