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