let A, B be Ordinal; :: thesis: ( A c= B iff succ A c= succ B )
( A c= B iff A in succ B ) by ORDINAL1:34;
hence ( A c= B iff succ A c= succ B ) by ORDINAL1:33; :: thesis: verum