:: deftheorem defaxpl1 defines axpl1 PL_AXIOM:def 22 :
for A being Element of PL-WFF holds
( A is axpl1 iff ex p, q being Element of PL-WFF st A = p => (q => p) );