let n, m be Nat; :: thesis: ( card n c= card m iff n <= m )
reconsider n = n, m = m as Element of NAT by ORDINAL1:def 13;
( ( card n c= card m implies card n c= card m ) & ( card n c= card m implies card n c= card m ) & card n = n & card m = m & ( n c= m implies n <= m ) & ( n <= m implies n c= m ) ) by Th40, CARD_1:def 5;
hence ( card n c= card m iff n <= m ) ; :: thesis: verum