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:22;
hence ( A c= B iff succ A c= succ B ) by ORDINAL1:21; :: thesis: verum