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