theorem Th9: :: INTPRO_1:9

for X being Subset of MC-wff
for p being Element of MC-wff holds FALSUM => p in CnIPC X