let g be ConwayGame; :: thesis:

hereby :: thesis:

assume A1: g is fuzzy ; :: thesis:

hereby :: thesis:

consider gL being ConwayGame such that
A2: ( gL in the_LeftOptions_of g & ( for gLR being ConwayGame st gLR in the_RightOptions_of gL holds
not gLR is nonpositive ) ) by A1, Th44;
take gL = gL; :: thesis:
thus gL in the_LeftOptions_of g by A2; :: thesis:
for gLR being ConwayGame holds
( not gLR in the_RightOptions_of gL or gLR is fuzzy or gLR is positive ) by A2;
hence gL is nonnegative by Th45; :: thesis:

end;

hereby :: thesis:

consider gR being ConwayGame such that
A3: ( gR in the_RightOptions_of g & ( for gRL being ConwayGame st gRL in the_LeftOptions_of gR holds
not gRL is nonnegative ) ) by A1, Th43;
take gR = gR; :: thesis:
thus gR in the_RightOptions_of g by A3; :: thesis:
for gRL being ConwayGame holds
( not gRL in the_LeftOptions_of gR or gRL is fuzzy or gRL is negative ) by A3;
hence gR is nonpositive by Th45; :: thesis:

end;

end;

hereby :: thesis:

assume ex gL being ConwayGame st
( gL in the_LeftOptions_of g & gL is nonnegative ) ; :: thesis:
then consider gL being ConwayGame such that
A4: ( gL in the_LeftOptions_of g & gL is nonnegative ) ;
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 gL is fuzzy & not gL is negative & not gR is fuzzy & not gR is positive ) by A4, A5;
then ( not g is nonpositive & not g is nonnegative ) by Th45, A4, A5;
hence g is fuzzy ; :: thesis:

end;