let g1, g2 be ConwayGame; :: thesis: ( g1 in the_proper_Tree_of g2 implies the_Tree_of g1 c= the_proper_Tree_of g2 )
assume A1: g1 in the_proper_Tree_of g2 ; :: thesis: the_Tree_of g1 c= the_proper_Tree_of g2
then A2: ( g1 in the_Tree_of g2 & g1 <> g2 ) by ZFMISC_1:56;
A3: the_Tree_of g1 c= the_Tree_of g2 by Th31, A1;
not g2 in the_Tree_of g1
proof
A4: ConwayRank g1 in ConwayRank g2 by A2, Th28;
assume g2 in the_Tree_of g1 ; :: thesis: contradiction
then ConwayRank g2 c= ConwayRank g1 by Th29;
then ConwayRank g1 in ConwayRank g1 by A4;
hence contradiction ; :: thesis: verum
end;
hence the_Tree_of g1 c= the_proper_Tree_of g2 by A3, ZFMISC_1:34; :: thesis: verum