let B1, B2 be Subset of (Election (A,n,B,k)); :: thesis: ( ( for f being FinSequence holds
( f in B1 iff f is A,n,B,k -dominated-election ) ) & ( for f being FinSequence holds
( f in B2 iff f is A,n,B,k -dominated-election ) ) implies B1 = B2 )
assume that
A1: for f being FinSequence holds
( f in B1 iff f is A,n,B,k -dominated-election ) and
A2: for f being FinSequence holds
( f in B2 iff f is A,n,B,k -dominated-election ) ; :: thesis: B1 = B2
thus B1 c= B2 by A1, A2; :: according to XBOOLE_0:def 10 :: thesis: B2 c= B1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B2 or x in B1 )
thus ( not x in B2 or x in B1 ) by A2, A1; :: thesis: verum