theorem Th42: :: CARD_1:44

for n being Nat holds nextcard (card n) = card (succ n)