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