let x be set ; :: thesis: Subtrees (x -tree {}) = {(x -tree {})}
dom (x -tree {}) = elementary_tree 0 by TREES_4:10, FUNCT_6:23, TREES_3:52;
then x -tree {} = root-tree ((x -tree {}) . {}) by TREES_4:5
.= root-tree x by TREES_4:def 4 ;
hence Subtrees (x -tree {}) = {(x -tree {})} by Th2; :: thesis: verum