let N, M be Cardinal; :: thesis: ( nextcard N = nextcard M implies M = N )
A1: card N = N by CARD_1:def 2;
card M = M by CARD_1:def 2;
hence ( nextcard N = nextcard M implies M = N ) by A1, Th105; :: thesis: verum