theorem ThL7: :: MSAFREE5:18

for c1, c2 being set
for d being DecoratedTree st c1 <> c2 holds
((root-tree c1),c2) <- d = root-tree c1