theorem :: ORDINAL1:37

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