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 a in union { (still_not-bound_in p) where p is Element of CQC-WFF : p in X } ; :: thesis: a in bound_QC-variables
then consider b being set such that
A1: ( a in b & 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 A1;
hence a in bound_QC-variables by A1; :: 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