set W = GRZ-formula-set ;
defpred S1[ object , object ] means ex t, u being GRZ-formula st
( t = $1 & u = $2 & t LD-= u );
A1: for a being object st a in GRZ-formula-set holds
S1[a,a] ;
A10: for a, b being object st S1[a,b] holds
S1[b,a] ;
A20: for a, b, c being object st S1[a,b] & S1[b,c] holds
S1[a,c]
proof
let a, b, c be object ; :: thesis: ( S1[a,b] & S1[b,c] implies S1[a,c] )
assume that
A21: S1[a,b] and
A22: S1[b,c] ; :: thesis: S1[a,c]
consider t, u being GRZ-formula such that
A23: ( t = a & u = b & t LD-= u ) by A21;
consider v, w being GRZ-formula such that
A26: ( v = b & w = c & v LD-= w ) by A22;
take t ; :: thesis: ex u being GRZ-formula st
( t = a & u = c & t LD-= u )
take w ; :: thesis: ( t = a & w = c & t LD-= w )
thus ( t = a & w = c & t LD-= w ) by A23, A26, Th74; :: thesis: verum
end;
consider E being Equivalence_Relation of GRZ-formula-set such that
A30: for a, b being object holds
( [a,b] in E iff ( a in GRZ-formula-set & b in GRZ-formula-set & S1[a,b] ) ) from EQREL_1:sch 1(A1, A10, A20);
 take E ; :: thesis: for t, u being GRZ-formula holds
( [t,u] in E iff t LD-= u )
let t, u be GRZ-formula; :: thesis: ( [t,u] in E iff t LD-= u )
thus ( [t,u] in E implies t LD-= u ) :: thesis: ( t LD-= u implies [t,u] in E )
proof
assume [t,u] in E ; :: thesis: t LD-= u
then consider v, w being GRZ-formula such that
A31: ( v = t & w = u & v LD-= w ) by A30;
thus t LD-= u by A31; :: thesis: verum
end;
thus ( t LD-= u implies [t,u] in E ) by A30; :: thesis: verum