theorem Th4: :: MSAFREE4:4

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