theorem Th8: :: CGAMES_1:8

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 ) )