theorem Th72: :: INTPRO_1:72

for X being Subset of MC-wff holds X c= CnCPC X