let EqR1, EqR2 be Equivalence_Relation of (the_Edges_of G); :: thesis: ( ( for e1, e2 being object holds
( [e1,e2] in EqR1 iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) ) & ( for e1, e2 being object holds
( [e1,e2] in EqR2 iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) ) implies EqR1 = EqR2 )
assume that
A10: for e1, e2 being object holds
( [e1,e2] in EqR1 iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) and
A11: for e1, e2 being object holds
( [e1,e2] in EqR2 iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) ; :: thesis: EqR1 = EqR2

now :: thesis: for e1, e2 being object holds
( [e1,e2] in EqR1 iff [e1,e2] in EqR2 )

let e1, e2 be object ; :: thesis: ( [e1,e2] in EqR1 iff [e1,e2] in EqR2 )
( [e1,e2] in EqR1 iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) by A10;
hence ( [e1,e2] in EqR1 iff [e1,e2] in EqR2 ) by A11; :: thesis: verum

end;

hence EqR1 = EqR2 by RELAT_1:def 2; :: thesis: verum