theorem :: GLIB_000:172
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)}