theorem Th80: :: INTPRO_2:79

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