let M, N be Cardinal; :: thesis: ( N in M iff nextcard N c= M )
A1: N in nextcard N by CARD_1:18;
card N = N ;
hence ( N in M iff nextcard N c= M ) by A1, CARD_1:def 3; :: thesis: verum