theorem Th12: :: INTPRO_1:12

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