theorem :: NAT_1:42

for n being Nat holds nextcard (card (Segm n)) = card (Segm (n + 1))