theorem Th17: :: ORDINAL1:21

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