theorem Th3: :: GLIB_013:3

for G being Dsimple _Graph ex f being one-to-one Function st
( dom f = the_Edges_of G & rng f c= [:(the_Vertices_of G),(the_Vertices_of G):] \ (id (the_Vertices_of G)) & ( for e being object st e in dom f holds
f . e = [((the_Source_of G) . e),((the_Target_of G) . e)] ) )