for n, k being Nat
for A, B being object st ( A = B or n <= k ) holds
DominatedElection (A,n,B,k) is empty