let n, k be Nat; 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 ; for f being FinSequence st f is A,n,B,k -dominated-election holds
n > k
let f be FinSequence; ( f is A,n,B,k -dominated-election implies n > k )
assume A1:
f is A,n,B,k -dominated-election
; 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; verum