theorem Th15: :: BALLOT_1:16

for n being Nat
for A, B being object st A <> B & n > 0 holds
n |-> A is A,n,B, 0 -dominated-election