let X, Y be Subset of CQC-WFF ; :: thesis: ( X c= Y implies still_not-bound_in X c= still_not-bound_in Y )
set A = { (still_not-bound_in p) where p is Element of CQC-WFF : p in X } ;
assume A1: X c= Y ; :: thesis: still_not-bound_in X c= still_not-bound_in Y

now

let a be set ; :: thesis: ( a in still_not-bound_in X implies a in still_not-bound_in Y )
assume A2: a in still_not-bound_in X ; :: thesis: a in still_not-bound_in Y
consider b being set such that
A3: ( a in b & b in { (still_not-bound_in p) where p is Element of CQC-WFF : p in X } ) by A2, TARSKI:def 4;
consider p being Element of CQC-WFF such that
A4: ( b = still_not-bound_in p & p in X ) by A3;
b in { (still_not-bound_in q) where q is Element of CQC-WFF : q in Y } by A1, A4;
hence a in still_not-bound_in Y by A3, TARSKI:def 4; :: thesis: verum

end;

hence still_not-bound_in X c= still_not-bound_in Y by TARSKI:def 3; :: thesis: verum