theorem :: CGAMES_1:49

for g being ConwayGame holds
( g is negative iff ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ex gR being ConwayGame st
( gR in the_RightOptions_of g & gR is nonpositive ) ) )