:: deftheorem Def3 defines nextcard CARD_1:def 3 :
for X being set
for b₂ being Cardinal holds
( b₂ = nextcard X iff ( card X in b₂ & ( for M being Cardinal st card X in M holds
b₂ c= M ) ) );