theorem :: INTPRO_1:93

for T being Subset of MC-wff st T is S4_theory holds
S4-Taut c= T