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