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