:: deftheorem Def93 defines '=' GRZLOG_1:def 45 :
for x, y, b₃ being LD-EqClass holds
( b₃ = x '=' y iff ex t, u being GRZ-formula st
( x = LD-EqClassOf t & y = LD-EqClassOf u & b₃ = LD-EqClassOf (t '=' u) ) );