theorem :: CARD_1:41

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