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