let g be ConwayGame; :: thesis:

hereby :: thesis:

assume A1: g is positive ; :: thesis:
hence A2: for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) by Th45; :: thesis:
consider gL being ConwayGame such that
A3: ( gL in the_LeftOptions_of g & not gL is fuzzy & not gL is negative ) by Th47, A1, A2;
take gL = gL; :: thesis:
thus ( gL in the_LeftOptions_of g & gL is nonnegative ) by A3; :: thesis:

end;

hereby :: thesis:

assume for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ; :: thesis:
then A4: g is nonnegative by Th45;
assume ex gL being ConwayGame st
( gL in the_LeftOptions_of g & gL is nonnegative ) ; :: thesis:
then consider gL being ConwayGame such that
A5: ( gL in the_LeftOptions_of g & gL is nonnegative ) ;
( not gL is fuzzy & not gL is negative ) by A5;
then not g is zero by Th47, A5;
hence g is positive by A4; :: thesis:

end;