theorem Th2: :: MSAFREE4:2

for x being set holds Subtrees (root-tree x) = {(root-tree x)}