let A be Ordinal; :: thesis: for R, S being Relation st R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
Day (R,A) = Day (S,A)
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]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
let R, S be Relation; :: thesis: ( R /\ [:(BeforeGames D),(BeforeGames D):] = S /\ [:(BeforeGames D),(BeforeGames D):] implies Day (R,D) c= Day (S,D) )
assume A3: R /\ [:(BeforeGames D),(BeforeGames D):] = S /\ [:(BeforeGames D),(BeforeGames D):] ; :: thesis: Day (R,D) c= Day (S,D)
let x1, x2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x1,x2] in Day (R,D) or [x1,x2] in Day (S,D) )
assume A4: [x1,x2] in Day (R,D) ; :: thesis: [x1,x2] in Day (S,D)
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

proof

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

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

proof

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

end;

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

end;

A16: for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
let R, S be Relation; :: thesis: ( R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] implies Day (R,A) = Day (S,A) )
assume A17: R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] ; :: thesis: Day (R,A) = Day (S,A)
( 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: verum