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