let k be Element of 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 A1: ( card X = k + 1 & x in X ) ; :: thesis: card (X \ {x}) = k
then card X = card (k + 1) ;
then reconsider X' = X as finite set ;
set Xx = X' \ {x};
{x} c= X by A1, ZFMISC_1:37;
then {x} /\ X = {x} by XBOOLE_1:28;
then ( {x} misses X' \ {x} & (X' \ {x}) \/ {x} = X ) by XBOOLE_1:51, XBOOLE_1:79;
then ( (card {x}) + (card (X' \ {x})) = k + 1 & card {x} = 1 ) by A1, CARD_1:50, CARD_2:53;
hence card (X \ {x}) = k ; :: thesis: verum