:: deftheorem defines neg^4 INTPRO_2:def 13 :
for p being Element of MC-wff holds neg^4 p = (((p => FALSUM) => FALSUM) => FALSUM) => FALSUM;