theorem Th2: :: GROUP_10:2

for E being non empty finite set
for k being Element of NAT
for x1, x2 being set st x1 <> x2 holds
card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E))