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