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