for x being object
for D being non empty set
for T being finite binary DecoratedTree of D st T = root-tree x holds
Leaves T = {x}