:: deftheorem defines root-tree TREES_4:def 2 :
for x being object holds root-tree x = (elementary_tree 0) --> x;