theorem :: INTPRO_1:76

for T being Subset of MC-wff st T is CPC_theory holds
CPC-Taut c= T