for T being DecoratedTree st dom T = elementary_tree 0 holds
T = root-tree (T . {}) by TARSKI:def 1, TREES_1:29;