:: deftheorem Def1 defines Election BALLOT_1:def 1 :
for A being object
for n being Nat
for B being object
for k being Nat
for b₅ being Subset of ((n + k) -tuples_on {A,B}) holds
( b₅ = Election (A,n,B,k) iff for v being Element of (n + k) -tuples_on {A,B} holds
( v in b₅ iff card (v " {A}) = n ) );