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