let X, Y be Subset of (bound_QC-variables Al); :: thesis: ( ( for a being object holds

( a in X iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) & ( for a being object holds

( a in Y iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) implies X = Y )

assume that

A2: for a being object holds

( a in X iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) ) and

A3: for a being object holds

( a in Y iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) ) ; :: thesis: X = Y

( a in X iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) & ( for a being object holds

( a in Y iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) ) ) implies X = Y )

assume that

A2: for a being object holds

( a in X iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) ) and

A3: for a being object holds

( a in Y iff ex i being Nat ex p being Element of CQC-WFF Al st

( i in dom f & p = f . i & a in still_not-bound_in p ) ) ; :: thesis: X = Y

now :: thesis: for a being object holds

( a in X iff a in Y )

hence
X = Y
by TARSKI:2; :: thesis: verum( a in X iff a in Y )

let a be object ; :: thesis: ( a in X iff a in Y )

( a in X iff ex i being Nat ex p being Element of CQC-WFF Al 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;( a in X iff ex i being Nat ex p being Element of CQC-WFF Al 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