theorem Th15: :: CARD_FIN:16

for X being finite set
for k being Nat
for x, y being object st x <> y holds
card (Choose (X,k,x,y)) = (card X) choose k