theorem Th81: :: INTPRO_1:81

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