:: deftheorem defines => GRZLOG_1:def 15 :
for t, u being GRZ-formula holds t => u = t '=' (t '&' u);