theorem Th80: :: INTPRO_1:80

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