let g be ConwayGame; :: thesis: ( ( g is nonnegative implies for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) & ( ( for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) implies g is nonnegative ) & ( g is nonpositive implies for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) implies g is nonpositive ) )
defpred S₂[ ConwayGame] means ( ( $1 is nonnegative implies for gR being ConwayGame holds
( not gR in the_RightOptions_of $1 or gR is fuzzy or gR is positive ) ) & ( ( for gR being ConwayGame holds
( not gR in the_RightOptions_of $1 or gR is fuzzy or gR is positive ) ) implies $1 is nonnegative ) & ( $1 is nonpositive implies for gL being ConwayGame holds
( not gL in the_LeftOptions_of $1 or gL is fuzzy or gL is negative ) ) & ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of $1 or gL is fuzzy or gL is negative ) ) implies $1 is nonpositive ) );
A1: for g being ConwayGame st ( for gO being ConwayGame st gO in the_Options_of g holds
S₂[gO] ) holds
S₂[g]

proof

let g be ConwayGame; :: thesis: ( ( for gO being ConwayGame st gO in the_Options_of g holds
S₂[gO] ) implies S₂[g] )
assume A2: for gO being ConwayGame st gO in the_Options_of g holds
S₂[gO] ; :: thesis: S₂[g]

hereby :: thesis: ( ( ( for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) implies g is nonnegative ) & ( g is nonpositive implies for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) implies g is nonpositive ) )

assume A3: g is nonnegative ; :: thesis: for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive )
let gR be ConwayGame; :: thesis: ( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive )
assume A4: gR in the_RightOptions_of g ; :: thesis: ( gR is fuzzy or gR is positive )
consider gRL being ConwayGame such that
A5: ( gRL in the_LeftOptions_of gR & gRL is nonnegative ) by A3, A4, Th43;

now

gR in the_Options_of g by A4, XBOOLE_0:def 3;
hence S₂[gR] by A2; :: thesis: ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & not gRL is fuzzy & not gRL is negative )

hereby :: thesis: verum

take gRL = gRL; :: thesis: ( gRL in the_LeftOptions_of gR & not gRL is fuzzy & not gRL is negative )
thus gRL in the_LeftOptions_of gR by A5; :: thesis: ( not gRL is fuzzy & not gRL is negative )
thus ( not gRL is fuzzy & not gRL is negative ) by A5; :: thesis: verum

end;

end;

then ( not gR is negative & not gR is zero ) ;
hence ( gR is fuzzy or gR is positive ) by Th42; :: thesis: verum

end;

hereby :: thesis: ( g is nonpositive iff for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) )

assume A6: for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ; :: thesis: g is nonnegative

now

let gR be ConwayGame; :: thesis: ( gR in the_RightOptions_of g implies ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL is nonnegative ) )
assume A7: gR in the_RightOptions_of g ; :: thesis: ex gRL being ConwayGame st
( gRL in the_LeftOptions_of gR & gRL is nonnegative )

now

gR in the_Options_of g by A7, XBOOLE_0:def 3;
hence S₂[gR] by A2; :: thesis: not gR is nonpositive
( gR is fuzzy or gR is positive ) by A6, A7;
hence not gR is nonpositive ; :: thesis: verum

end;

then consider gRL being ConwayGame such that
A8: ( gRL in the_LeftOptions_of gR & not gRL is fuzzy & not gRL is negative ) ;
take gRL = gRL; :: thesis: ( gRL in the_LeftOptions_of gR & gRL is nonnegative )
( gRL is zero or gRL is positive ) by A8, Th42;
hence ( gRL in the_LeftOptions_of gR & gRL is nonnegative ) by A8; :: thesis: verum

end;

hence g is nonnegative by Th43; :: thesis: verum

end;

hereby :: thesis: ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) implies g is nonpositive )

assume A9: g is nonpositive ; :: thesis: for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative )
let gL be ConwayGame; :: thesis: ( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative )
assume A10: gL in the_LeftOptions_of g ; :: thesis: ( gL is fuzzy or gL is negative )
consider gLR being ConwayGame such that
A11: ( gLR in the_RightOptions_of gL & gLR is nonpositive ) by A9, A10, Th44;

now

gL in the_Options_of g by A10, XBOOLE_0:def 3;
hence S₂[gL] by A2; :: thesis: ex gLR being ConwayGame st
( gLR in the_RightOptions_of gL & not gLR is fuzzy & not gLR is positive )

hereby :: thesis: verum

take gLR = gLR; :: thesis: ( gLR in the_RightOptions_of gL & not gLR is fuzzy & not gLR is positive )
thus gLR in the_RightOptions_of gL by A11; :: thesis: ( not gLR is fuzzy & not gLR is positive )
thus ( not gLR is fuzzy & not gLR is positive ) by A11; :: thesis: verum

end;

end;

then ( not gL is positive & not gL is zero ) ;
hence ( gL is fuzzy or gL is negative ) by Th42; :: thesis: verum

end;

hereby :: thesis: verum

assume A12: for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ; :: thesis: g is nonpositive

now

let gL be ConwayGame; :: thesis: ( gL in the_LeftOptions_of g implies ex gLR being ConwayGame st
( gLR in the_RightOptions_of gL & gLR is nonpositive ) )
assume A13: gL in the_LeftOptions_of g ; :: thesis: ex gLR being ConwayGame st
( gLR in the_RightOptions_of gL & gLR is nonpositive )

now

gL in the_Options_of g by A13, XBOOLE_0:def 3;
hence S₂[gL] by A2; :: thesis: not gL is nonnegative
( gL is fuzzy or gL is negative ) by A12, A13;
hence not gL is nonnegative ; :: thesis: verum

end;

then consider gLR being ConwayGame such that
A14: ( gLR in the_RightOptions_of gL & not gLR is fuzzy & not gLR is positive ) ;
take gLR = gLR; :: thesis: ( gLR in the_RightOptions_of gL & gLR is nonpositive )
( gLR is zero or gLR is negative ) by A14, Th42;
hence ( gLR in the_RightOptions_of gL & gLR is nonpositive ) by A14; :: thesis: verum

end;

hence g is nonpositive by Th44; :: thesis: verum

end;

end;

for g being ConwayGame holds S₂[g] from CGAMES_1:sch 3(A1);
hence ( ( g is nonnegative implies for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) & ( ( for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) implies g is nonnegative ) & ( g is nonpositive implies for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) implies g is nonpositive ) ) ; :: thesis: verum