theorem :: BALLOT_1:20

for n, k being Nat
for A, B being object st n > k & A <> B holds
(n |-> A) ^ (k |-> B) in DominatedElection (A,n,B,k)