:: deftheorem defines => MODAL_1:def 13 :
for A, B being MP-wff holds A => B = 'not' (A '&' ('not' B));