theorem :: BALLOT_1:28

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