let g be ConwayGame; :: thesis:

hereby :: thesis:

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

end;

hereby :: thesis:

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

end;