let k be Nat; :: thesis: for X, x being set st card X = k + 1 & x in X holds
card (X \ {x}) = k
let X, x be set ; :: thesis: ( card X = k + 1 & x in X implies card (X \ {x}) = k )
assume that
A1: card X = k + 1 and
A2: x in X ; :: thesis: card (X \ {x}) = k
reconsider X9 = X as finite set by A1;
set Xx = X9 \ {x};
{x} c= X by A2, ZFMISC_1:31;
then {x} /\ X = {x} by XBOOLE_1:28;
then (X9 \ {x}) \/ {x} = X by XBOOLE_1:51;
then A3: (card {x}) + (card (X9 \ {x})) = k + 1 by A1, CARD_2:40, XBOOLE_1:79;
card {x} = 1 by CARD_1:30;
hence card (X \ {x}) = k by A3; :: thesis: verum