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, m = m as Element of omega by ORDINAL1:def 13;
( card n = n & card m = m ) by Def5;
hence n = m by A1; :: thesis: verum