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();
A2: 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 A3: a in Y ; :: thesis: a in CQC-WFF
thus a in CQC-WFF by A1, A3; :: thesis: verum

end;

reconsider Z = Y as Subset of CQC-WFF by A2;
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