let k be Nat; :: thesis: for X being finite set st k <= card X holds

ex Y being Subset of X st card Y = k

let X be finite set ; :: thesis: ( k <= card X implies ex Y being Subset of X st card Y = k )

assume k <= card X ; :: thesis: ex Y being Subset of X st card Y = k

then Segm (card k) c= Segm (card X) by NAT_1:39;

then consider Y being set such that

A1: Y c= X and

A2: card Y = card k by CARD_FIL:36;

reconsider Y = Y as Subset of X by A1;

take Y ; :: thesis: card Y = k

thus card Y = k by A2; :: thesis: verum

ex Y being Subset of X st card Y = k

let X be finite set ; :: thesis: ( k <= card X implies ex Y being Subset of X st card Y = k )

assume k <= card X ; :: thesis: ex Y being Subset of X st card Y = k

then Segm (card k) c= Segm (card X) by NAT_1:39;

then consider Y being set such that

A1: Y c= X and

A2: card Y = card k by CARD_FIL:36;

reconsider Y = Y as Subset of X by A1;

take Y ; :: thesis: card Y = k

thus card Y = k by A2; :: thesis: verum