:: deftheorem defaxpl3 defines axpl3 PL_AXIOM:def 24 :
for A being Element of PL-WFF holds
( A is axpl3 iff ex p, q being Element of PL-WFF st A = (('not' q) => ('not' p)) => ((('not' q) => p) => q) );