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