theorem :: TREES_3:62

for T being Tree holds elementary_tree 1 c= ^ T