theorem :: TREES_3:71

for T1, T2 being Tree holds elementary_tree 2 c= tree (T1,T2)