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