let n be natural number ; :: 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:78;
assume not the_subsets_of_card n,X is empty ; :: thesis: contradiction
then consider x being set 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 card (Seg n) c= card X by A2, CARD_1:27;
then card (Seg n) <= card X by NAT_1:40;
hence contradiction by A1, FINSEQ_1:78; :: thesis: verum