defpred S₁[ set ] means for T being Subset of CQC-WFF st T is being_a_theory & X c= T holds
$1 in T;
consider Y being set such that
A1: for a being set holds
( a in Y iff ( a in CQC-WFF & S₁[a] ) ) from XBOOLE_0:sch 1();
Y c= CQC-WFF

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in CQC-WFF )
assume a in Y ; :: thesis: a in CQC-WFF
hence a in CQC-WFF by A1; :: thesis: verum

end;

then reconsider Z = Y as Subset of CQC-WFF ;
take Z ; :: thesis: for t being Element of CQC-WFF holds
( t in Z iff for T being Subset of CQC-WFF st T is being_a_theory & X c= T holds
t in T )
thus for t being Element of CQC-WFF holds
( t in Z iff for T being Subset of CQC-WFF st T is being_a_theory & X c= T holds
t in T ) by A1; :: thesis: verum