theorem :: INTPRO_1:16

for T being Subset of MC-wff st T is IPC_theory holds
IPC-Taut c= T