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