theorem :: TREES_3:42

for T1, T2 being Tree st T1 -level 1 c= T2 -level 1 & ( for n being Element of NAT st <*n*> in T1 holds
T1 | <*n*> = T2 | <*n*> ) holds
T1 c= T2