let T1, T2 be Tree; :: thesis: ( T1 -level 1 c= T2 -level 1 & ( for n being Element of NAT st <*n*> in T1 holds
T1 | <*n*> = T2 | <*n*> ) implies T1 c= T2 )
assume that
A1: T1 -level 1 c= T2 -level 1 and
A2: for n being Element of NAT st <*n*> in T1 holds
T1 | <*n*> = T2 | <*n*> ; :: thesis: T1 c= T2
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T1 or x in T2 )
assume x in T1 ; :: thesis: x in T2
then reconsider t = x as Element of T1 ;

now :: thesis: ( t <> {} implies t in T2 )

assume t <> {} ; :: thesis: t in T2
then consider p being FinSequence of NAT , n being Element of NAT such that
A3: t = <*n*> ^ p by FINSEQ_2:130;
A4: len <*n*> = 1 by FINSEQ_1:39;
reconsider n = n as Element of NAT ;
reconsider q = <*n*> as Element of T1 by A3, TREES_1:21;
A5: q in T1 -level 1 by A4;
then A6: q in T2 -level 1 by A1;
A7: p in T1 | q by A3, TREES_1:def 6;
T1 | <*n*> = T2 | <*n*> by A2, A5;
hence t in T2 by A3, A6, A7, TREES_1:def 6; :: thesis: verum

end;

hence x in T2 by TREES_1:22; :: thesis: verum