let M, N be Cardinal; :: thesis: ( N in nextcard M iff N c= M )
A1: ( not N c= M iff M in N ) by CARD_1:4;
( N in nextcard M iff not nextcard M c= N ) by CARD_1:4;
hence ( N in nextcard M iff N c= M ) by A1, Th87; :: thesis: verum