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