let g1, g2 be ConwayGame; :: thesis: ( g1 in the_Tree_of g2 implies the_proper_Tree_of g1 c= the_proper_Tree_of g2 )
assume A1: g1 in the_Tree_of g2 ; :: thesis: the_proper_Tree_of g1 c= the_proper_Tree_of g2
then A2: the_Tree_of g1 c= the_Tree_of g2 by Th31;

hereby :: according to TARSKI:def 3 :: thesis: verum

let x be set ; :: thesis: ( x in the_proper_Tree_of g1 implies x in the_proper_Tree_of g2 )
assume A3: x in the_proper_Tree_of g1 ; :: thesis: x in the_proper_Tree_of g2
then A4: ( x in the_Tree_of g1 & x <> g1 ) by ZFMISC_1:56;
assume A5: not x in the_proper_Tree_of g2 ; :: thesis: contradiction
then A6: x = g2 by A2, A4, ZFMISC_1:56;

per cases ( g1 = g2 or ConwayRank g1 in ConwayRank g2 ) by Th28, A1;

suppose g1 = g2 ; :: thesis: contradiction

hence contradiction by A3, A5; :: thesis: verum

end;

suppose A7: ConwayRank g1 in ConwayRank g2 ; :: thesis: contradiction

reconsider g = x as ConwayGame by A3;
ConwayRank g in ConwayRank g2 by A7, Th29, A4, ORDINAL1:12;
hence contradiction by A6; :: thesis: verum

end;

end;

end;