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