theorem :: GLIBPRE1:21
for G being _Graph
for e being object st e in the_Edges_of G holds
e in G .edgesBetween {((the_Source_of G) . e),((the_Target_of G) . e)}