:: deftheorem defines => HILBERT1:def 8 :
for p, q being Element of HP-WFF holds p => q = (<*1*> ^ p) ^ q;