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