theorem :: CARD_FIN:9

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