let n, m be natural number ; :: thesis: ( card n = card m implies n = m )
assume A1: card n = card m ; :: thesis: n = m
reconsider n = n as Element of omega by ORDINAL1:def 12;
card n = n by Def5;
hence n = m by A1, Def5; :: thesis: verum