theorem :: CARD_1:15

for X being set holds {} in nextcard X