let n be natural number ; :: thesis: for E being non empty set st card n c= card E holds
not the_subsets_of_card n,E is empty
let E be non empty set ; :: thesis: ( card n c= card E implies not the_subsets_of_card n,E is empty )
assume card n c= card E ; :: thesis: not the_subsets_of_card n,E is empty
then consider f being Function such that
A1: ( f is one-to-one & dom f = n & rng f c= E ) by CARD_1:26;
set X = f .: n;
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
A2: rng f = f .: n by A1, RELAT_1:146;
then n,f .: n are_equipotent by A1, WELLORD2:def 4;
then card (f .: n) = card n' by CARD_1:21;
then card (f .: n) = n' by CARD_1:def 5;
then f .: n in { X' where X' is Subset of E : card X' = n } by A1, A2;
hence not the_subsets_of_card n,E is empty ; :: thesis: verum