let g, gO be ConwayGame; :: thesis: ( gO in the_Options_of g implies the_Tree_of gO c= the_proper_Tree_of g )
assume A1: gO in the_Options_of g ; :: thesis: the_Tree_of gO c= the_proper_Tree_of g
the_Options_of g c= the_proper_Tree_of g by Th33;
hence the_Tree_of gO c= the_proper_Tree_of g by Th35, A1; :: thesis: verum