theorem :: TREES_3:63

for T1, T2 being Tree st T1 c= T2 holds
^ T1 c= ^ T2