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