let x be set ; :: thesis: ( x in the_LeftOptions_of ConwayOne iff x = ConwayZero )
the_LeftOptions_of ConwayOne = {ConwayZero} by Def6;
hence ( x in the_LeftOptions_of ConwayOne iff x = ConwayZero ) by TARSKI:def 1; :: thesis: verum