dom (root-tree x) = elementary_tree 0 by TREES_4:3;
hence ( root-tree x is finite & root-tree x is root ) by Def1; :: thesis: verum