:: deftheorem defines 'not' PL_AXIOM:def 9 :
for p being Element of PL-WFF holds 'not' p = p => FaLSUM;