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