defpred S₁[ object ] means for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
$1 in T;
consider Y being set such that
A1: for a being object holds
( a in Y iff ( a in CQC-WFF Al & S₁[a] ) ) from XBOOLE_0:sch 1();
Y c= CQC-WFF Al by A1;
then reconsider Z = Y as Subset of (CQC-WFF Al) ;
take Z ; :: thesis: for t being Element of CQC-WFF Al holds
( t in Z iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
t in T )
thus for t being Element of CQC-WFF Al holds
( t in Z iff for T being Subset of (CQC-WFF Al) st T is being_a_theory & X c= T holds
t in T ) by A1; :: thesis: verum