:: deftheorem Def23 defines CnS4 INTPRO_1:def 23 :
for X, b₂ being Subset of MC-wff holds
( b₂ = CnS4 X iff for r being Element of MC-wff holds
( r in b₂ iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) );