defpred S₁[ object ] means ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st $1 = Ex (x,p);
consider X being set such that
A1: for a being object holds
( a in X iff ( a in CQC-WFF Al & S₁[a] ) ) from XBOOLE_0:sch 1();
for a being object st a in X holds
a in CQC-WFF Al by A1;
then reconsider X = X as Subset of (CQC-WFF Al) by TARSKI:def 3;
take X ; :: thesis: for a being set holds
( a in X iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) )
thus for a being set holds
( a in X iff ex x being bound_QC-variable of Al ex p being Element of CQC-WFF Al st a = Ex (x,p) ) by A1; :: thesis: verum