for X being set
for x being object holds
( x in succ X iff ( x in X or x = X ) )