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 12;
( card n = n & card m = m ) by CARD_1:def 2;
hence ( card n c= card m iff n <= m ) by Th40; :: thesis: verum