:: deftheorem defines => PL_AXIOM:def 5 :
for p, q being Element of PL-WFF holds p => q = (<*1*> ^ p) ^ q;