let n, m be natural number ; :: thesis: ( card n c= card m iff n c= m )
( card n = n & card m = m ) by Def5;
hence ( card n c= card m iff n c= m ) ; :: thesis: verum