theorem Th11: :: MSAFREE4:11

for x being set
for p being DTree-yielding FinSequence holds rng p c= Subtrees (x -tree p)