set Y = union { (still_not-bound_in p) where p is Element of CQC-WFF : p in X } ;

now

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

end;

hence union { (still_not-bound_in p) where p is Element of CQC-WFF : p in X } is Subset of bound_QC-variables by TARSKI:def 3; :: thesis: verum