let p, q be Element of MC-wff ; |-_IPC (((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM)) => (((p => q) => FALSUM) => FALSUM)
(p => q) => FALSUM in {((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))}
by TARSKI:def 2;
then A1:
{((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))} |-_IPC (p => q) => FALSUM
by Th67;
((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM) in {((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))}
by TARSKI:def 2;
then A2:
{((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))} |-_IPC ((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM)
by Th67;
A03:
|-_IPC ((p => FALSUM) 'or' q) => (p => q)
by Th80;
A04:
{} MC-wff c= {((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))}
;
|-_IPC (((p => FALSUM) 'or' q) => (p => q)) => (((p => q) => FALSUM) => (((p => FALSUM) 'or' q) => FALSUM))
by Th81;
then
|-_IPC ((p => q) => FALSUM) => (((p => FALSUM) 'or' q) => FALSUM)
by A03, Th37;
then
{((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))} |-_IPC ((p => q) => FALSUM) => (((p => FALSUM) 'or' q) => FALSUM)
by A04, Th66;
then A4:
{((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))} |-_IPC ((p => FALSUM) 'or' q) => FALSUM
by A1, Th27;
A07:
|-_IPC (((p => FALSUM) 'or' q) => FALSUM) => (((p => FALSUM) => FALSUM) '&' (q => FALSUM))
by Th97;
{((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))} |-_IPC (((p => FALSUM) 'or' q) => FALSUM) => (((p => FALSUM) => FALSUM) '&' (q => FALSUM))
by A04, A07, Th66;
then A6:
{((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))} |-_IPC ((p => FALSUM) => FALSUM) '&' (q => FALSUM)
by A4, Th27;
{((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))} |-_IPC (((p => FALSUM) => FALSUM) '&' (q => FALSUM)) => ((p => FALSUM) => FALSUM)
by Th20;
then
{((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))} |-_IPC (p => FALSUM) => FALSUM
by A6, Th27;
then A8:
{((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))} |-_IPC (q => FALSUM) => FALSUM
by A2, Th27;
{((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))} |-_IPC (((p => FALSUM) => FALSUM) '&' (q => FALSUM)) => (q => FALSUM)
by Th21;
then
{((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))} |-_IPC q => FALSUM
by A6, Th27;
then
{((p => q) => FALSUM),(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))} |-_IPC FALSUM
by A8, Th27;
then
{(((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))} |-_IPC ((p => q) => FALSUM) => FALSUM
by Th55;
hence
|-_IPC (((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM)) => (((p => q) => FALSUM) => FALSUM)
by Th54; verum