let n, m be Nat; :: thesis: ( card n c= card m iff n c= m )
card n = n by Def2;
hence ( card n c= card m iff n c= m ) by Def2; :: thesis: verum