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:

let gLR be ConwayGame; :: thesis:
assume gLR in the_RightOptions_of gL ; :: thesis:
then ( not gLR is negative & not gLR is zero ) by A2;
hence ( gLR is fuzzy or gLR is positive ) by Th42; :: thesis:

end;

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:

let gRL be ConwayGame; :: thesis:
assume gRL in the_LeftOptions_of gR ; :: thesis:
then ( not gRL is positive & not gRL is zero ) by A3;
hence ( gRL is fuzzy or gRL is negative ) by Th42; :: thesis:

end;

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;