for n being Nat
for E being non empty set st card n c= card E holds
not the_subsets_of_card (n,E) is empty