let E1, E2 be Equivalence_Relation of GRZ-formula-set; ( ( for t, u being GRZ-formula holds
( [t,u] in E1 iff t LD-= u ) ) & ( for t, u being GRZ-formula holds
( [t,u] in E2 iff t LD-= u ) ) implies E1 = E2 )
assume that
A1:
for t, u being GRZ-formula holds
( [t,u] in E1 iff t LD-= u )
and
A2:
for t, u being GRZ-formula holds
( [t,u] in E2 iff t LD-= u )
; E1 = E2
for t, u being GRZ-formula holds
( [t,u] in E1 iff [t,u] in E2 )
by A1, A2;
hence
E1 = E2
by RELSET_1:def 2; verum