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
assume not the_subsets_of_card n,X is empty ; :: thesis: contradiction
then consider x being set such that
A2: x in the_subsets_of_card n,X by XBOOLE_0:def 1;
consider X' being Subset of X such that
A3: ( x = X' & card X' = n ) by A2;
A4: card (Seg n) = n by FINSEQ_1:78;
card (Seg n) c= card X by A3, A4, CARD_1:27;
then card (Seg n) <= card X by NAT_1:40;
hence contradiction by A1, FINSEQ_1:78; :: thesis: verum