let g be ConwayGame; :: thesis: ( g is zero iff ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) ) )
thus ( g is zero implies ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) ) ) by Th45; :: thesis: ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) implies g is zero )
assume ( ( for gL being ConwayGame holds
( not gL in the_LeftOptions_of g or gL is fuzzy or gL is negative ) ) & ( for gR being ConwayGame holds
( not gR in the_RightOptions_of g or gR is fuzzy or gR is positive ) ) ) ; :: thesis: g is zero
then ( g is nonpositive & g is nonnegative ) by Th45;
hence g is zero ; :: thesis: verum