let E1, E2 be Equivalence_Relation of GRZ-formula-set; :: thesis: ( ( 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 ) ; :: thesis: 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; :: thesis: verum