let g be ConwayGame; :: thesis: ( g is nonpositive iff for gL being ConwayGame st gL in the_LeftOptions_of g holds
ex gLR being ConwayGame st
( gLR in the_RightOptions_of gL & gLR is nonpositive ) )

hereby :: thesis: ( ( for gL being ConwayGame st gL in the_LeftOptions_of g holds
ex gLR being ConwayGame st
( gLR in the_RightOptions_of gL & gLR is nonpositive ) ) implies g is nonpositive )

assume g is nonpositive ; :: thesis: for gL being ConwayGame st gL in the_LeftOptions_of g holds
ex gLR being set st
( gLR in the_RightOptions_of gL & gLR is nonpositive )
then A1: - g is nonnegative ;
let gL be ConwayGame; :: thesis: ( gL in the_LeftOptions_of g implies ex gLR being set st
( gLR in the_RightOptions_of gL & gLR is nonpositive ) )
assume gL in the_LeftOptions_of g ; :: thesis: ex gLR being set st
( gLR in the_RightOptions_of gL & gLR is nonpositive )
then - gL in the_RightOptions_of (- g) by Th39;
then consider gRL being ConwayGame such that
A2: ( gRL in the_LeftOptions_of (- gL) & gRL is nonnegative ) by A1, Th43;
take gLR = - gRL; :: thesis: ( gLR in the_RightOptions_of gL & gLR is nonpositive )
( gLR in the_RightOptions_of (- (- gL)) & - (- gL) = gL & - gLR = gRL ) by A2, Th39, Th40;
hence ( gLR in the_RightOptions_of gL & gLR is nonpositive ) by A2; :: thesis: verum

end;

assume A3: for gL being ConwayGame st gL in the_LeftOptions_of g holds
ex gLR being ConwayGame st
( gLR in the_RightOptions_of gL & gLR is nonpositive ) ; :: thesis: g is nonpositive

now :: thesis: for gR being ConwayGame st gR in the_RightOptions_of (- g) holds
ex gRL being set st
( gRL in the_LeftOptions_of gR & gRL is nonnegative )

let gR be ConwayGame; :: thesis: ( gR in the_RightOptions_of (- g) implies ex gRL being set st
( gRL in the_LeftOptions_of gR & gRL is nonnegative ) )
assume gR in the_RightOptions_of (- g) ; :: thesis: ex gRL being set st
( gRL in the_LeftOptions_of gR & gRL is nonnegative )
then ( - gR in the_LeftOptions_of (- (- g)) & - (- g) = g ) by Th39, Th40;
then consider gLR being ConwayGame such that
A4: ( gLR in the_RightOptions_of (- gR) & gLR is nonpositive ) by A3;
take gRL = - gLR; :: thesis: ( gRL in the_LeftOptions_of gR & gRL is nonnegative )
( gRL in the_LeftOptions_of (- (- gR)) & - (- gR) = gR ) by A4, Th39, Th40;
hence ( gRL in the_LeftOptions_of gR & gRL is nonnegative ) by A4; :: thesis: verum

end;

then - g is nonnegative by Th43;
hence g is nonpositive ; :: thesis: verum