:: deftheorem Def17 defines negative MODAL_1:def 17 :
for IT being MP-wff holds
( IT is negative iff ex A being MP-wff st IT = 'not' A );