for t, u being GRZ-formula holds
( t LD-= u iff LD-EqClassOf t = LD-EqClassOf u )