theorem :: CARD_1:40

for m, n being Nat st card n = card m holds
n = m ;