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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the_proper_Tree_of g1 or 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;