theorem Th1: :: GLIB_013:1

for G being non-Dmulti _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):] & ( for e being object st e in dom f holds
f . e = [((the_Source_of G) . e),((the_Target_of G) . e)] ) )