:: deftheorem defines neg INTPRO_1:def 17 :
for p being Element of MC-wff holds neg p = p => FALSUM;