:: deftheorem Def76 defines LD-= GRZLOG_1:def 38 :
for t, u being GRZ-formula holds
( t LD-= u iff t '=' u is LD-provable );