defpred S_{1}[ 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_{1}[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

$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

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