let g be ConwayGame; :: thesis:
defpred S₂[ set ] means for g being ConwayGame st g in $1 holds
for gR being ConwayGame st gR in the_RightOptions_of g holds
ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL in $1 );
A1: for s being set
for alpha being Ordinal st S₂[s] holds
S₂[s /\ (ConwayDay alpha)]

proof

let s be set ; :: thesis:
let alpha be Ordinal; :: thesis:
assume A2: S₂[s] ; :: thesis:
let g be ConwayGame; :: thesis:
assume g in s /\ (ConwayDay alpha) ; :: thesis:
then A3: ( g in s & g in ConwayDay alpha ) by XBOOLE_0:def 4;
let gR be ConwayGame; :: thesis:
assume A4: gR in the_RightOptions_of g ; :: thesis:
then consider gRL being ConwayGame such that
A5: ( gRL in the_LeftOptions_of gR & gRL in s ) by A2, A3;
take gRL ; :: thesis:
gR in ConwayDay alpha by Th11, A3, A4;
then gRL in ConwayDay alpha by Th11, A5;
hence ( gRL in the_LeftOptions_of gR & gRL in s /\ (ConwayDay alpha) ) by A5, XBOOLE_0:def 4; :: thesis:

end;

hereby :: thesis:

assume g is nonnegative ; :: thesis:
then consider s being set such that
A6: ( g in s & S₂[s] ) ;
let gR be ConwayGame; :: thesis:
assume gR in the_RightOptions_of g ; :: thesis:
then consider gRL being ConwayGame such that
A7: ( gRL in the_LeftOptions_of gR & gRL in s ) by A6;
take gRL = gRL; :: thesis:
thus gRL in the_LeftOptions_of gR by A7; :: thesis:
thus gRL is nonnegative by A6, A7; :: thesis:

end;

hereby :: thesis:

assume A8: for gR being ConwayGame st gR in the_RightOptions_of g holds
ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL is nonnegative ) ; :: thesis:
consider alpha being Ordinal such that
A9: g in ConwayDay alpha by Def3;

now :: thesis:

set ss = { s1 where s1 is Subset of (ConwayDay alpha) : S₂[s1] } ;
take s = union { s1 where s1 is Subset of (ConwayDay alpha) : S₂[s1] } ; :: thesis:
A10: S₂[s]

proof

let g1 be ConwayGame; :: thesis:
assume g1 in s ; :: thesis:
then consider s2 being set such that
A11: ( g1 in s2 & s2 in { s1 where s1 is Subset of (ConwayDay alpha) : S₂[s1] } ) by TARSKI:def 4;
consider s1 being Subset of (ConwayDay alpha) such that
A12: ( s1 = s2 & S₂[s1] ) by A11;
let gR be ConwayGame; :: thesis:
assume gR in the_RightOptions_of g1 ; :: thesis:
then consider gRL being ConwayGame such that
A13: ( gRL in the_LeftOptions_of gR & gRL in s1 ) by A11, A12;
take gRL ; :: thesis:
s2 c= s by A11, ZFMISC_1:74;
hence ( gRL in the_LeftOptions_of gR & gRL in s ) by A12, A13; :: thesis:

end;

thus g in s :: thesis:

proof

now :: thesis:

let x be set ; :: thesis:
assume x in { s1 where s1 is Subset of (ConwayDay alpha) : S₂[s1] } ; :: thesis:
then ex s1 being Subset of (ConwayDay alpha) st
( x = s1 & S₂[s1] ) ;
hence x c= ConwayDay alpha ; :: thesis:

end;

then A14: s c= ConwayDay alpha by ZFMISC_1:76;
{g} c= ConwayDay alpha by A9, ZFMISC_1:31;
then reconsider sg = s \/ {g} as Subset of (ConwayDay alpha) by A14, XBOOLE_1:8;
S₂[sg]

proof

let g1 be ConwayGame; :: thesis:
assume A15: g1 in sg ; :: thesis:
let gR be ConwayGame; :: thesis:
assume A16: gR in the_RightOptions_of g1 ; :: thesis:

per cases by A15, XBOOLE_0:def 3;

suppose g1 in s ; :: thesis:

then consider gRL being ConwayGame such that
A17: ( gRL in the_LeftOptions_of gR & gRL in s ) by A10, A16;
take gRL ; :: thesis:
thus gRL in the_LeftOptions_of gR by A17; :: thesis:
s c= sg by XBOOLE_1:7;
hence gRL in sg by A17; :: thesis:

end;

suppose g1 in {g} ; :: thesis:

then g1 = g by TARSKI:def 1;
then consider gRL being ConwayGame such that
A18: ( gRL in the_LeftOptions_of gR & gRL is nonnegative ) by A8, A16;
consider s0 being set such that
A19: ( gRL in s0 & S₂[s0] ) by A18;
take gRL ; :: thesis:
thus gRL in the_LeftOptions_of gR by A18; :: thesis:
reconsider s1 = s0 /\ (ConwayDay alpha) as Subset of (ConwayDay alpha) by XBOOLE_1:17;
S₂[s1] by A19, A1;
then s1 in { s1 where s1 is Subset of (ConwayDay alpha) : S₂[s1] } ;
then A20: s1 c= s by ZFMISC_1:74;
gR in ConwayDay alpha by A15, A16, Th11;
then gRL in ConwayDay alpha by A18, Th11;
then gRL in s1 by A19, XBOOLE_0:def 4;
hence gRL in sg by A20, XBOOLE_0:def 3; :: thesis:

end;

end;

end;

then A21: sg in { s1 where s1 is Subset of (ConwayDay alpha) : S₂[s1] } ;
g in {g} by TARSKI:def 1;
then g in sg by XBOOLE_0:def 3;
hence g in s by A21, TARSKI:def 4; :: thesis:

end;

thus S₂[s] by A10; :: thesis:

end;

hence g is nonnegative ; :: thesis:

end;