theorem Th71: :: INTPRO_1:71

for T, X being Subset of MC-wff st T is CPC_theory & X c= T holds
CnCPC X c= T by Def20;