theorem Th3: :: MSAFREE4:3

for x being set
for p being non empty DTree-yielding FinSequence holds Subtrees (x -tree p) = {(x -tree p)} \/ (Subtrees (rng p))