theorem Th13: :: ORDINAL1:17

for x being set st x is Ordinal holds
succ x is Ordinal