let X1, X2 be set ; :: thesis: ( ( for b being set holds
( b in X1 iff ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) ) & ( for b being set holds
( b in X2 iff ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) ) implies X1 = X2 )
assume A2: ( ( for b being set holds
( b in X1 iff ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) ) & ( for b being set holds
( b in X2 iff ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) ) ) ; :: thesis: X1 = X2

now

let b be set ; :: thesis: ( b in X1 iff b in X2 )
( ( b in X1 implies ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) & ( ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) implies b in X1 ) & ( b in X2 implies ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) & ( ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) implies b in X2 ) ) by A2;
hence ( b in X1 iff b in X2 ) ; :: thesis: verum

end;

hence X1 = X2 by TARSKI:2; :: thesis: verum