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)

proof

let z be object ; :: thesis: ( z in { (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } implies z in CQC-WFF (FCEx Al) )
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: z in CQC-WFF (FCEx Al)
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: verum

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: verum