now :: thesis: ( ex gL being Element of ConwayDay 0 st
( gL in the_LeftOptions_of ConwayStar & gL is nonnegative ) & ex gR being Element of ConwayDay 0 st
( gR in the_RightOptions_of ConwayStar & gR is nonpositive ) )

hereby :: thesis: ex gR being Element of ConwayDay 0 st
( gR in the_RightOptions_of ConwayStar & gR is nonpositive )

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

end;

hereby :: thesis: verum

take gR = ConwayZero ; :: thesis: ( gR in the_RightOptions_of ConwayStar & gR is nonpositive )
thus gR in the_RightOptions_of ConwayStar by Th8; :: thesis: gR is nonpositive
thus gR is nonpositive ; :: thesis: verum

end;

end;

hence ConwayStar is fuzzy by Th46; :: thesis: verum