theorem Th3: :: TREES_4:3

for x being object holds
( dom (root-tree x) = elementary_tree 0 & (root-tree x) . {} = x )