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