theorem Th5: :: ORDINAL1:9

for X being set holds X <> succ X