theorem Th24: :: BALLOT_1:24

for n, k being Nat
for d being XFinSequence of NAT holds
( d in Domin_0 ((n + k),k) iff <*0*> ^ (XFS2FS d) in DominatedElection (0,(n + 1),1,k) )