:: deftheorem defines limit_cardinal CARD_1:def 4 :
for M being Cardinal holds
( M is limit_cardinal iff for N being Cardinal holds not M = nextcard N );