let O be Ordinal; :: thesis: 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 R be Relation; :: thesis: 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 A be Element of Games O; :: thesis: ( A in Day (R,O) iff ( L_ A << R, R_ A & ( for o being object st o in (L_ A) \/ (R_ A) holds
ex A being Ordinal st
( A in O & o in Day (R,A) ) ) ) )
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: ( L_ A << R, R_ A & ( for o being object st o in (L_ A) \/ (R_ A) holds
ex A being Ordinal st
( A in O & o in Day (R,A) ) ) implies A in Day (R,O) )

proof

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

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: A in Day (R,O)
A13: (L_ A) \/ (R_ A) c= union (rng (L | O))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (L_ A) \/ (R_ A) or x in union (rng (L | O)) )
assume A14: x in (L_ A) \/ (R_ A) ; :: thesis: x in union (rng (L | O))
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: verum

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: verum