theorem :: CARD_5:25

for n being Nat holds
( cf 0 = 0 & cf (card (n + 1)) = 1 )