defpred S₁[ object ] means for T being Subset of MC-wff st T is S4_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 MC-wff & S₁[a] ) ) from XBOOLE_0:sch 1();
Y c= MC-wff by A1;
then reconsider Z = Y as Subset of MC-wff ;
take Z ; :: thesis: for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T )
thus for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) by A1; :: thesis: verum