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