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