for A, B being Ordinal holds
( A in B iff succ A in succ B )