theorem Th1: :: ORDINAL2:1

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