theorem Th7: :: MSAFREE4:7

for x, y being set
for p being DTree-yielding FinSequence st p is finite-yielding holds
for t being DecoratedTree st x in Subtrees t & t in rng p holds
x <> y -tree p