set gL = ConwayZero ;
( ConwayZero in the_LeftOptions_of ConwayStar & ConwayZero is nonnegative & ConwayZero in the_RightOptions_of ConwayStar & ConwayZero is nonpositive ) by Th8;
hence ConwayStar is fuzzy by Th46; :: thesis: verum