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