:: deftheorem Def3 defines DominatedElection BALLOT_1:def 3 :
for A being object
for n being Nat
for B being object
for k being Nat
for b₅ being Subset of (Election (A,n,B,k)) holds
( b₅ = DominatedElection (A,n,B,k) iff for f being FinSequence holds
( f in b₅ iff f is A,n,B,k -dominated-election ) );