:: deftheorem defines 'or' PL_AXIOM:def 12 :
for p, q being Element of PL-WFF holds p 'or' q = ('not' p) => q;