theorem Th82: :: INTPRO_2:81

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