let M, N be Cardinal; :: thesis: ( nextcard N = nextcard M implies M = N )
A1: card N = N ;
card M = M ;
hence ( nextcard N = nextcard M implies M = N ) by A1, Th85; :: thesis: verum