let A be finite set ; :: thesis: for x being set st x in A holds
card (A \ {x}) = (card A) - (card {x})
let x be set ; :: thesis: ( x in A implies card (A \ {x}) = (card A) - (card {x}) )
assume x in A ; :: thesis: card (A \ {x}) = (card A) - (card {x})
then {x} c= A by ZFMISC_1:37;
hence card (A \ {x}) = (card A) - (card {x}) by CARD_2:63; :: thesis: verum