theorem Th1: :: INTPRO_1:1

for X being Subset of MC-wff
for p, q being Element of MC-wff holds p => (q => p) in CnIPC X