theorem Th88: :: INTPRO_1:88

for T, X being Subset of MC-wff st T is S4_theory & X c= T holds
CnS4 X c= T by Def23;