theorem Th11: :: BALLOT_1:12

for n, k being Nat
for A, B being object
for v being Element of (n + k) -tuples_on {A,B} st A <> B holds
( v in Election (A,n,B,k) iff card (v " {B}) = k )