set gL = ConwayZero ;
( ConwayZero in the_LeftOptions_of ConwayOne & ConwayZero is nonnegative & ( for gR being ConwayGame holds
( not gR in the_RightOptions_of ConwayOne or gR is fuzzy or gR is positive ) ) ) by Th7;
hence ConwayOne is positive by Th48; :: thesis: verum