:: deftheorem defines '&' GRZLOG_1:def 12 :
for t, u being GRZ-formula holds t '&' u = (Polish-binOp (GRZ-symbols,GRZ-arity,'&')) . (t,u);