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