theorem :: CGAMES_1:36

for g, gO being ConwayGame st gO in the_Options_of g holds
the_Tree_of gO c= the_proper_Tree_of g