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