let p, q be Element of MC-wff ; :: thesis: |-_IPC ((p 'or' q) => FALSUM) => ((p => FALSUM) '&' (q => FALSUM))
A1: (((p 'or' q) => FALSUM) => (p => FALSUM)) => ((((p 'or' q) => FALSUM) => (q => FALSUM)) => (((p 'or' q) => FALSUM) => ((p => FALSUM) '&' (q => FALSUM)))) in IPC-Taut by INTPRO_1:38;
A2: (p => (p 'or' q)) => (((p 'or' q) => FALSUM) => (p => FALSUM)) in IPC-Taut by INTPRO_1:24;
p => (p 'or' q) in IPC-Taut by INTPRO_1:def 14;
then A3: ((p 'or' q) => FALSUM) => (p => FALSUM) in IPC-Taut by A2, INTPRO_1:def 14;
A4: (q => (p 'or' q)) => (((p 'or' q) => FALSUM) => (q => FALSUM)) in IPC-Taut by INTPRO_1:24;
q => (p 'or' q) in IPC-Taut by INTPRO_1:def 14;
then A5: ((p 'or' q) => FALSUM) => (q => FALSUM) in IPC-Taut by A4, INTPRO_1:def 14;
(((p 'or' q) => FALSUM) => (q => FALSUM)) => (((p 'or' q) => FALSUM) => ((p => FALSUM) '&' (q => FALSUM))) in IPC-Taut by A1, A3, INTPRO_1:def 14;
then ((p 'or' q) => FALSUM) => ((p => FALSUM) '&' (q => FALSUM)) in IPC-Taut by A5, INTPRO_1:def 14;
hence |-_IPC ((p 'or' q) => FALSUM) => ((p => FALSUM) '&' (q => FALSUM)) by Th69; :: thesis: verum