let n, k be Nat; :: thesis: for A, B being object
for f being FinSequence st f is A,n,B,k -dominated-election holds
n > k
let A, B be object ; :: thesis: for f being FinSequence st f is A,n,B,k -dominated-election holds
n > k
let f be FinSequence; :: thesis: ( f is A,n,B,k -dominated-election implies n > k )
assume A1: f is A,n,B,k -dominated-election ; :: thesis: n > k
then reconsider f = f as Element of (n + k) -tuples_on {A,B} ;
(len f) + 1 >= len f by NAT_1:13;
then A2: f | ((len f) + 1) = f by FINSEQ_1:58;
A3: A <> B by A1, Th13;
A4: card (f " {A}) = n by A1, Def1;
card (f " {B}) = k by A1, A3, Th11;
hence n > k by A2, A1, A4; :: thesis: verum