for z being object st z in { (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } holds
z in CQC-WFF (FCEx Al)

let z be object ; :: thesis:
assume A1: z in { (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ; :: thesis:
ex p being Element of CQC-WFF Al ex x being bound_QC-variable of Al st z = Example_Formula_of (p,x) by A1;
hence z in CQC-WFF (FCEx Al) ; :: thesis:

end;

hence { (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } is Subset of (CQC-WFF (FCEx Al)) by TARSKI:def 3; :: thesis: