let O be Ordinal; :: thesis: 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 object ; :: thesis: ( 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 ) ) ) )
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: ( 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 ) ) implies o in Games O )

proof

assume o in Games O ; :: thesis: ( 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 ) ) )
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: for x being object st x in (L_ o) \/ (R_ o) holds
ex B being Ordinal st
( B in O & x in Games B )
let z be object ; :: thesis: ( z in (L_ o) \/ (R_ o) implies ex B being Ordinal st
( B in O & z in Games B ) )
assume A7: z in (L_ o) \/ (R_ o) ; :: thesis: ex B being Ordinal st
( B in O & z in Games B )
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: ( OO in O & z in Games OO )
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: verum

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: o in Games O
A13: (L_ o) \/ (R_ o) c= union (rng (L | O))

proof

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

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