theorem Th26: :: BALLOT_1:26

for n, k being Nat holds card (Domin_0 ((n + k),k)) = card (DominatedElection (0,(n + 1),1,k))