let p be Element of MC-wff ; :: thesis: |-_IPC p => ((p => FALSUM) => FALSUM)
p => FALSUM in {(p => FALSUM),p} by TARSKI:def 2;
then A1: {(p => FALSUM),p} |-_IPC p => FALSUM by Th67;
p in {(p => FALSUM),p} by TARSKI:def 2;
then {(p => FALSUM),p} |-_IPC p by Th67;
then {(p => FALSUM),p} |-_IPC FALSUM by A1, Th27;
then {p} |-_IPC (p => FALSUM) => FALSUM by Th55;
then |-_IPC p => ((p => FALSUM) => FALSUM) by Th54;
hence |-_IPC p => ((p => FALSUM) => FALSUM) ; :: thesis: verum