theorem Th99: :: INTPRO_2:98

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