theorem Th1: :: CARD_5:1

for X being set holds nextcard (card X) = nextcard X