theorem Th4: :: EXCHSORT:4

for x being set holds (succ x) \ x = {x}