theorem Th2: :: ORDINAL1:6

for X being set holds X in succ X