let g be ConwayGame; :: thesis:
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]

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

hereby :: thesis:

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

gR in the_Options_of g by A4, XBOOLE_0:def 3;
hence S₂[gR] by A2; :: thesis:

hereby :: thesis:

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

end;

end;

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

end;

hereby :: thesis:

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

let gR be ConwayGame; :: thesis:
assume A7: gR in the_RightOptions_of g ; :: thesis:

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

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:
thus ( gRL in the_LeftOptions_of gR & gRL is nonnegative ) by A8; :: thesis:

end;

hence g is nonnegative by Th43; :: thesis:

end;

hereby :: thesis:

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

gL in the_Options_of g by A10, XBOOLE_0:def 3;
hence S₂[gL] by A2; :: thesis:

hereby :: thesis:

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

end;

end;

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

end;

hereby :: thesis:

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

let gL be ConwayGame; :: thesis:
assume A13: gL in the_LeftOptions_of g ; :: thesis:

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

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:
thus ( gLR in the_RightOptions_of gL & gLR is nonpositive ) by A14; :: thesis:

end;

hence g is nonpositive by Th44; :: thesis:

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: