let g be ConwayGame; :: thesis: the_Options_of g c= the_Tree_of g
the_Options_of g c= the_proper_Tree_of g by Th33;
hence the_Options_of g c= the_Tree_of g by XBOOLE_1:1; :: thesis: verum