let M, N be Cardinal; :: thesis: ( M in N iff ( M c= N & M <> N ) )
( M c< N iff ( M c= N & M <> N ) ) by XBOOLE_0:def 8;
hence ( M in N iff ( M c= N & M <> N ) ) by ORDINAL1:21, ORDINAL1:def 2; :: thesis: verum