theorem Th40: :: CARD_2:41

for x being object
for X being finite set st not x in X holds
card (X \/ {x}) = (card X) + 1