let EqR1, EqR2 be Equivalence_Relation of (the_Edges_of G); ( ( for e1, e2 being object holds
( [e1,e2] in EqR1 iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) ) & ( for e1, e2 being object holds
( [e1,e2] in EqR2 iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) ) implies EqR1 = EqR2 )
assume that
A21:
for e1, e2 being object holds
( [e1,e2] in EqR1 iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) )
and
A22:
for e1, e2 being object holds
( [e1,e2] in EqR2 iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) )
; EqR1 = EqR2
now for e1, e2 being object holds
( [e1,e2] in EqR1 iff [e1,e2] in EqR2 )let e1,
e2 be
object ;
( [e1,e2] in EqR1 iff [e1,e2] in EqR2 )
(
[e1,e2] in EqR1 iff ex
v1,
v2 being
object st
(
e1 DJoins v1,
v2,
G &
e2 DJoins v1,
v2,
G ) )
by A21;
hence
(
[e1,e2] in EqR1 iff
[e1,e2] in EqR2 )
by A22;
verum end;
hence
EqR1 = EqR2
by RELAT_1:def 2; verum