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