let p, q be Element of MC-wff ; :: thesis: |-_IPC q => (((p '&' q) => FALSUM) => (p => FALSUM))
p in {p,((p '&' q) => FALSUM),q} by ENUMSET1:def 1;
then A1: {p,((p '&' q) => FALSUM),q} |-_IPC p by Th67;
(p '&' q) => FALSUM in {p,((p '&' q) => FALSUM),q} by ENUMSET1:def 1;
then A2: {p,((p '&' q) => FALSUM),q} |-_IPC (p '&' q) => FALSUM by Th67;
q in {p,((p '&' q) => FALSUM),q} by ENUMSET1:def 1;
then A3: {p,((p '&' q) => FALSUM),q} |-_IPC q by Th67;
A04: |-_IPC p => (q => (p '&' q)) by Th22;
{} MC-wff c= {p,((p '&' q) => FALSUM),q} ;
then {p,((p '&' q) => FALSUM),q} |-_IPC p => (q => (p '&' q)) by A04, Th66;
then {p,((p '&' q) => FALSUM),q} |-_IPC q => (p '&' q) by A1, Th27;
then {p,((p '&' q) => FALSUM),q} |-_IPC p '&' q by A3, Th27;
then {p,((p '&' q) => FALSUM),q} |-_IPC FALSUM by A2, Th27;
then {((p '&' q) => FALSUM),q} |-_IPC p => FALSUM by Th56;
then {q} |-_IPC ((p '&' q) => FALSUM) => (p => FALSUM) by Th55;
hence |-_IPC q => (((p '&' q) => FALSUM) => (p => FALSUM)) by Th54; :: thesis: verum