let t, u be GRZ-formula; :: thesis: ( t LD-= u iff LD-EqClassOf t = LD-EqClassOf u )
thus ( t LD-= u implies LD-EqClassOf t = LD-EqClassOf u ) :: thesis: ( LD-EqClassOf t = LD-EqClassOf u implies t LD-= u )

proof

assume t LD-= u ; :: thesis: LD-EqClassOf t = LD-EqClassOf u
then [t,u] in LD-EqR by Def80;
then u in LD-EqClassOf t by EQREL_1:18;
hence LD-EqClassOf t = LD-EqClassOf u by EQREL_1:23; :: thesis: verum

end;

assume LD-EqClassOf t = LD-EqClassOf u ; :: thesis: t LD-= u
then u in LD-EqClassOf t by EQREL_1:23;
then [t,u] in LD-EqR by EQREL_1:18;
hence t LD-= u by Def80; :: thesis: verum