let X, Y be Subset of bound_QC-variables; :: thesis: ( ( for a being set holds
( a in X iff ex i being Element of NAT ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) & ( for a being set holds
( a in Y iff ex i being Element of NAT ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) implies X = Y )
assume that
A2: for a being set holds
( a in X iff ex i being Element of NAT ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) and
A3: for a being set holds
( a in Y iff ex i being Element of NAT ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) ; :: thesis: X = Y

now

let a be set ; :: thesis: ( a in X iff a in Y )
( a in X iff ex i being Element of NAT ex p being Element of CQC-WFF st
( i in dom f & p = f . i & a in still_not-bound_in p ) ) by A2;
hence ( a in X iff a in Y ) by A3; :: thesis: verum

end;

hence X = Y by TARSKI:2; :: thesis: verum