:: deftheorem Def80 defines LD-EqR GRZLOG_1:def 39 :
for b₁ being Equivalence_Relation of GRZ-formula-set holds
( b₁ = LD-EqR iff for t, u being GRZ-formula holds
( [t,u] in b₁ iff t LD-= u ) );