for g being ConwayGame holds
( ( g is nonnegative implies for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) & ( ( for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) implies g is nonnegative ) & ( g is nonpositive implies for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) implies g is nonpositive ) )