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