let n be Nat; :: 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 )
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
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 and
A2: dom f = n and
A3: rng f c= E by CARD_1:10;
set X = f .: n;
A4: rng f = f .: n by A2, RELAT_1:113;
then n,f .: n are_equipotent by A1, A2;
then card (f .: n) = n9 by CARD_1:def 2;
then f .: n in { X9 where X9 is Subset of E : card X9 = n } by A3, A4;
hence not the_subsets_of_card (n,E) is empty ; :: thesis: verum