for m, n being Nat holds
( card n c= card m iff n c= m ) ;