theorem Th89: :: INTPRO_1:89

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