theorem Th9: :: CARD_FIN:10

for X being finite set
for k being Nat
for x1, x2 being object st card X < k holds
Choose (X,k,x1,x2) is empty