for x being set holds
( ( 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 ) )