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 ;
( S1[a,b] & S1[b,c] implies S1[a,c] )
assume that A21:
S1[
a,
b]
and A22:
S1[
b,
c]
;
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
;
ex u being GRZ-formula st
( t = a & u = c & t LD-= u )
take
w
;
( t = a & w = c & t LD-= w )
thus
(
t = a &
w = c &
t LD-= w )
by A23, A26, Th74;
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
; for t, u being GRZ-formula holds
( [t,u] in E iff t LD-= u )
let t, u be GRZ-formula; ( [t,u] in E iff t LD-= u )
thus
( [t,u] in E implies t LD-= u )
( t LD-= u implies [t,u] in E )
thus
( t LD-= u implies [t,u] in E )
by A30; verum