for M, N being Cardinal holds
( M in N iff not N c= M ) by ORDINAL1:5, ORDINAL1:16;