theorem Th1: :: GROUP_10:1

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