let p, q be Element of MC-wff ; |-_IPC (((p => q) => FALSUM) => FALSUM) => (((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))
A01:
p in {p,(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)}
by ENUMSET1:def 2;
A1:
{p,(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)} |-_IPC p
by A01, Th67;
q => FALSUM in {p,(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)}
by ENUMSET1:def 2;
then A2:
{p,(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)} |-_IPC q => FALSUM
by Th67;
((p => q) => FALSUM) => FALSUM in {p,(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)}
by ENUMSET1:def 2;
then A3:
{p,(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)} |-_IPC ((p => q) => FALSUM) => FALSUM
by Th67;
{p,(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)} |-_IPC p => ((q => FALSUM) => (p '&' (q => FALSUM)))
by Th22;
then
{p,(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)} |-_IPC (q => FALSUM) => (p '&' (q => FALSUM))
by A1, Th27;
then A4:
{p,(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)} |-_IPC p '&' (q => FALSUM)
by A2, Th27;
A06:
|-_IPC (p '&' (q => FALSUM)) => ((p => q) => FALSUM)
by Th107;
A07:
{} MC-wff c= {p,(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)}
;
|-_IPC ((p '&' (q => FALSUM)) => ((p => q) => FALSUM)) => ((((p => q) => FALSUM) => FALSUM) => ((p '&' (q => FALSUM)) => FALSUM))
by Th81;
then
|-_IPC (((p => q) => FALSUM) => FALSUM) => ((p '&' (q => FALSUM)) => FALSUM)
by A06, Th37;
then
{p,(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)} |-_IPC (((p => q) => FALSUM) => FALSUM) => ((p '&' (q => FALSUM)) => FALSUM)
by A07, Th66;
then
{p,(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)} |-_IPC (p '&' (q => FALSUM)) => FALSUM
by A3, Th27;
then
{p,(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)} |-_IPC FALSUM
by A4, Th27;
then A8:
{(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)} |-_IPC p => FALSUM
by Th57;
(p => FALSUM) => FALSUM in {(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)}
by ENUMSET1:def 1;
then
{(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)} |-_IPC (p => FALSUM) => FALSUM
by Th67;
then
{(q => FALSUM),((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)} |-_IPC FALSUM
by A8, Th27;
then
{((p => FALSUM) => FALSUM),(((p => q) => FALSUM) => FALSUM)} |-_IPC (q => FALSUM) => FALSUM
by Th56;
then
{(((p => q) => FALSUM) => FALSUM)} |-_IPC ((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM)
by Th55;
hence
|-_IPC (((p => q) => FALSUM) => FALSUM) => (((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))
by Th54; verum