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