theorem :: CARD_1:48

for M being finite Cardinal ex n being Nat st M = card n