theorem Th18: :: ORDINAL1:22

for A, C being Ordinal holds
( A in succ C iff A c= C )