let n, k be Nat; :: thesis: for A, B being object st n > k & A <> B holds
(n |-> A) ^ (k |-> B) in DominatedElection (A,n,B,k)
let A, B be object ; :: thesis: ( n > k & A <> B implies (n |-> A) ^ (k |-> B) in DominatedElection (A,n,B,k) )
assume that
A1: n > k and
A2: A <> B ; :: thesis: (n |-> A) ^ (k |-> B) in DominatedElection (A,n,B,k)
k < n - 0 by A1;
then (n |-> A) ^ (k |-> B) is A,n,B,0 + k -dominated-election by Th16, A2, Th15;
hence (n |-> A) ^ (k |-> B) in DominatedElection (A,n,B,k) by Def3; :: thesis: verum