theorem :: INTPRO_1:79
for T being Subset of MC-wff st T is S4_theory holds
T is IPC_theory ;