theorem Th4: :: ORDINAL1:8

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