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 a in still_not-bound_in X ; :: thesis: a in still_not-bound_in Y
then consider b being set such that
A2: a in b and
A3: b in { (still_not-bound_in p) where p is Element of CQC-WFF : p in X } by TARSKI:def 4;
ex p being Element of CQC-WFF st
( b = still_not-bound_in p & p in X ) by A3;
then b in { (still_not-bound_in q) where q is Element of CQC-WFF : q in Y } by A1;
hence a in still_not-bound_in Y by A2, TARSKI:def 4; :: thesis: verum

end;

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