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

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