theorem Th27: :: BALLOT_1:27

for n, k being Nat
for A, B being object st A <> B & n > k holds
card (DominatedElection (A,n,B,k)) = ((n - k) / (n + k)) * ((n + k) choose k)