for T being Tree holds elementary_tree 1 c= ^ T