let p be Element of MC-wff ; :: thesis: |-_IPC FALSUM 'equiv' (p '&' (p => FALSUM))
A1: |-_IPC FALSUM => (p '&' (p => FALSUM)) by Th36;
|-_IPC (p '&' (p => FALSUM)) => FALSUM by Th100;
hence |-_IPC FALSUM 'equiv' (p '&' (p => FALSUM)) by A1, Th84; :: thesis: verum