theorem :: CARD_3:91

for M, N being Cardinal holds
( N in nextcard M iff N c= M )