theorem Th126: :: INTPRO_2:125

for p, q being Element of MC-wff holds |-_IPC p => ((p => FALSUM) => q)