let n, m be Nat; :: thesis: ( card n in card m iff n < m )
A1: ( ( n <= m & n <> m ) iff n < m ) by XXREAL_0:1;
( card n c< card m iff ( card n c= card m & card n <> card m ) ) by XBOOLE_0:def 8;
hence ( card n in card m iff n < m ) by A1, Th41, ORDINAL1:21, ORDINAL1:def 2; :: thesis: verum