:: deftheorem defines ? MODAL_1:def 11 :
for A being MP-wff holds ? A = 'not' ((#) ('not' A));