let n, k be Nat; :: thesis: for A, B being object st ( A = B or n <= k ) holds
DominatedElection (A,n,B,k) is empty
let A, B be object ; :: thesis: ( ( A = B or n <= k ) implies DominatedElection (A,n,B,k) is empty )
assume A1: ( A = B or n <= k ) ; :: thesis: DominatedElection (A,n,B,k) is empty
assume not DominatedElection (A,n,B,k) is empty ; :: thesis: contradiction
then consider f being object such that
A2: f in DominatedElection (A,n,B,k) ;
f in Election (A,n,B,k) by A2;
then reconsider f = f as Element of (n + k) -tuples_on {A,B} ;
f is A,n,B,k -dominated-election by A2, Def3;
hence contradiction by Th13, Th14, A1; :: thesis: verum