for M, N being Cardinal holds
( M in N iff ( M c= N & M <> N ) ) by ORDINAL1:11, XBOOLE_0:def 8;