theorem Th5: :: TREES_4:5

for T being DecoratedTree st dom T = elementary_tree 0 holds
T = root-tree (T . {})