:: deftheorem defines the_Options_of CGAMES_1:def 8 :
for g being ConwayGame holds the_Options_of g = (the_LeftOptions_of g) \/ (the_RightOptions_of g);