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