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

now :: thesis: for a being object st a in union { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X } holds
a in bound_QC-variables Al

let a be object ; :: thesis: ( a in union { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X } implies a in bound_QC-variables Al )
assume a in union { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in X } ; :: thesis: a in bound_QC-variables Al
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 Al : p in X } ) by TARSKI:def 4;
ex p being Element of CQC-WFF Al st
( b = still_not-bound_in p & p in X ) by A1;
hence a in bound_QC-variables Al by A1; :: thesis: verum

end;

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