let x be set ; :: thesis: ( ( x in the_Options_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_Options_of ConwayStar ) & ( x in the_LeftOptions_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_LeftOptions_of ConwayStar ) & ( x in the_RightOptions_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_RightOptions_of ConwayStar ) )
( the_LeftOptions_of ConwayStar = {ConwayZero} & the_RightOptions_of ConwayStar = {ConwayZero} ) by Def6, Def7;
hence ( ( x in the_Options_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_Options_of ConwayStar ) & ( x in the_LeftOptions_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_LeftOptions_of ConwayStar ) & ( x in the_RightOptions_of ConwayStar implies x = ConwayZero ) & ( x = ConwayZero implies x in the_RightOptions_of ConwayStar ) ) by TARSKI:def 1; :: thesis: verum