:: deftheorem defines Nes INTPRO_1:def 13 :
for p being Element of MC-wff holds Nes p = <*6*> ^ p;