:: deftheorem defines '&' INTPRO_1:def 11 :
for p, q being Element of MC-wff holds p '&' q = (<*2*> ^ p) ^ q;