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

the_subsets_of_card (n,X) is empty

let X be finite set ; :: thesis: ( card X < n implies the_subsets_of_card (n,X) is empty )

assume A1: card X < n ; :: thesis: the_subsets_of_card (n,X) is empty

A2: card (Seg n) = n by FINSEQ_1:57;

assume not the_subsets_of_card (n,X) is empty ; :: thesis: contradiction

then consider x being object such that

A3: x in the_subsets_of_card (n,X) by XBOOLE_0:def 1;

ex X9 being Subset of X st

( x = X9 & card X9 = n ) by A3;

then Segm (card (Seg n)) c= Segm (card X) by A2, CARD_1:11;

then card (Seg n) <= card X by NAT_1:39;

hence contradiction by A1, FINSEQ_1:57; :: thesis: verum

the_subsets_of_card (n,X) is empty

let X be finite set ; :: thesis: ( card X < n implies the_subsets_of_card (n,X) is empty )

assume A1: card X < n ; :: thesis: the_subsets_of_card (n,X) is empty

A2: card (Seg n) = n by FINSEQ_1:57;

assume not the_subsets_of_card (n,X) is empty ; :: thesis: contradiction

then consider x being object such that

A3: x in the_subsets_of_card (n,X) by XBOOLE_0:def 1;

ex X9 being Subset of X st

( x = X9 & card X9 = n ) by A3;

then Segm (card (Seg n)) c= Segm (card X) by A2, CARD_1:11;

then card (Seg n) <= card X by NAT_1:39;

hence contradiction by A1, FINSEQ_1:57; :: thesis: verum