let p, q be Element of MC-wff ; :: thesis: |-_IPC (q => (p => FALSUM)) 'equiv' ((p '&' q) => FALSUM)
A1: |-_IPC ((p '&' q) => FALSUM) => (q => (p => FALSUM)) by Th90;
|-_IPC (q => (p => FALSUM)) => ((p '&' q) => FALSUM) by Th91;
hence |-_IPC (q => (p => FALSUM)) 'equiv' ((p '&' q) => FALSUM) by A1, Th84; :: thesis: verum