theorem :: BALLOT_1:9

for n being Nat
for A being object holds Election (A,n,A,0) = {(n |-> A)}