now :: thesis: ( ( for gR being ConwayGame holds
( not gR in the_RightOptions_of ConwayOne or gR is fuzzy or gR is positive ) ) & ex gL being Element of ConwayDay 0 st
( gL in the_LeftOptions_of ConwayOne & gL is nonnegative ) )

thus for gR being ConwayGame holds
( not gR in the_RightOptions_of ConwayOne or gR is fuzzy or gR is positive ) ; :: thesis: ex gL being Element of ConwayDay 0 st
( gL in the_LeftOptions_of ConwayOne & gL is nonnegative )

hereby :: thesis: verum

take gL = ConwayZero ; :: thesis: ( gL in the_LeftOptions_of ConwayOne & gL is nonnegative )
thus gL in the_LeftOptions_of ConwayOne by Th7; :: thesis: gL is nonnegative
thus gL is nonnegative ; :: thesis: verum

end;

end;

hence ConwayOne is positive by Th48; :: thesis: verum