let x be object ; :: thesis: for X being finite set st not x in X holds
card (X \/ {x}) = (card X) + 1
let X be finite set ; :: thesis: ( not x in X implies card (X \/ {x}) = (card X) + 1 )
A1: card {x} = 1 by CARD_1:30;
assume not x in X ; :: thesis: card (X \/ {x}) = (card X) + 1
hence card (X \/ {x}) = (card X) + 1 by A1, Th39, ZFMISC_1:50; :: thesis: verum