:: deftheorem Def3 defines EdgeAdjEqRel GLIB_009:def 3 :
for G being _Graph
for b₂ being Equivalence_Relation of (the_Edges_of G) holds
( b₂ = EdgeAdjEqRel G iff for e1, e2 being object holds
( [e1,e2] in b₂ iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) );