( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of ConwayZero or gL is fuzzy or gL is negative ) ) & ( for gR being ConwayGame holds
( not gR in the_RightOptions_of ConwayZero or gR is fuzzy or gR is positive ) ) ) ;
hence ConwayZero is zero by Th47; :: thesis: verum