theorem :: INTPRO_1:74

for X being Subset of MC-wff holds CnCPC (CnCPC X) = CnCPC X