let D be finite set ; :: thesis: for k being Nat st card D = k + 1 holds

ex x being Element of D ex C being Subset of D st

( D = C \/ {x} & card C = k )

let k be Nat; :: thesis: ( card D = k + 1 implies ex x being Element of D ex C being Subset of D st

( D = C \/ {x} & card C = k ) )

assume A1: card D = k + 1 ; :: thesis: ex x being Element of D ex C being Subset of D st

( D = C \/ {x} & card C = k )

then D <> {} ;

then consider x being object such that

A2: x in D by XBOOLE_0:def 1;

reconsider C = D \ {x} as Subset of D ;

reconsider x = x as Element of D by A2;

take x ; :: thesis: ex C being Subset of D st

( D = C \/ {x} & card C = k )

take C ; :: thesis: ( D = C \/ {x} & card C = k )

x in {x} by TARSKI:def 1;

then A3: not x in C by XBOOLE_0:def 5;

{x} c= D by A2, ZFMISC_1:31;

hence D = C \/ {x} by XBOOLE_1:45; :: thesis: card C = k

then card D = (card C) + 1 by A3, CARD_2:41;

hence card C = k by A1; :: thesis: verum

ex x being Element of D ex C being Subset of D st

( D = C \/ {x} & card C = k )

let k be Nat; :: thesis: ( card D = k + 1 implies ex x being Element of D ex C being Subset of D st

( D = C \/ {x} & card C = k ) )

assume A1: card D = k + 1 ; :: thesis: ex x being Element of D ex C being Subset of D st

( D = C \/ {x} & card C = k )

then D <> {} ;

then consider x being object such that

A2: x in D by XBOOLE_0:def 1;

reconsider C = D \ {x} as Subset of D ;

reconsider x = x as Element of D by A2;

take x ; :: thesis: ex C being Subset of D st

( D = C \/ {x} & card C = k )

take C ; :: thesis: ( D = C \/ {x} & card C = k )

x in {x} by TARSKI:def 1;

then A3: not x in C by XBOOLE_0:def 5;

{x} c= D by A2, ZFMISC_1:31;

hence D = C \/ {x} by XBOOLE_1:45; :: thesis: card C = k

then card D = (card C) + 1 by A3, CARD_2:41;

hence card C = k by A1; :: thesis: verum