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