let g1, g2 be ConwayGame; :: thesis: ( g1 in the_Tree_of g2 implies the_Tree_of g1 c= the_Tree_of g2 )
assume g1 in the_Tree_of g2 ; :: thesis: the_Tree_of g1 c= the_Tree_of g2
then consider f2 being ConwayGameChain such that
A1: ( f2 . 1 = g1 & f2 . (len f2) = g2 ) by Def12;
hereby :: according to TARSKI:def 3 :: thesis: verum
let x be object ; :: thesis: ( x in the_Tree_of g1 implies b1 in the_Tree_of g2 )
assume x in the_Tree_of g1 ; :: thesis: b1 in the_Tree_of g2
then consider f1 being ConwayGameChain such that
A2: ( f1 . 1 = x & f1 . (len f1) = g1 ) by Def12;
A3: len f1 >= 1 by NAT_1:14;
per cases ( len f1 = 1 or len f1 > 1 ) by A3, XXREAL_0:1;
suppose A4: len f1 > 1 ; :: thesis: b1 in the_Tree_of g2
then reconsider n0 = (len f1) - 1 as non zero Nat by NAT_1:21;
reconsider f0 = f1 | n0 as ConwayGameChain by Th25;
( len f1 is Element of dom f1 & n0 <= len f1 ) by FINSEQ_5:6, XREAL_1:43;
then ( f1 . n0 in the_Options_of g1 & f0 . n0 = f1 . n0 & len f0 = n0 ) by Def11, A2, A4, FINSEQ_1:59, FINSEQ_3:112;
then reconsider f = f0 ^ f2 as ConwayGameChain by Th26, A1;
n0 >= 1 by NAT_1:14;
then ( 1 in dom f0 & len f2 in dom f2 & f0 . 1 = f1 . 1 & len f = (len f0) + (len f2) ) by FINSEQ_1:22, FINSEQ_3:112, FINSEQ_5:6;
then ( f . 1 = x & f . (len f) = g2 ) by A1, A2, FINSEQ_1:def 7;
hence x in the_Tree_of g2 by Def12; :: thesis: verum
end;
end;
end;