:: deftheorem defines '&' QC_LANG1:def 16 :
for A being QC-alphabet
for p, q being Element of QC-WFF A holds p '&' q = (<*[2,0]*> ^ (@ p)) ^ (@ q);