theorem Th4: :: TREES_9:4

for t being DecoratedTree holds
( t is root iff {} in Leaves (dom t) )