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