theorem Th4: :: GLIB_013:4

for G being non-multi _Graph ex f being one-to-one Function st
( dom f = the_Edges_of G & rng f c= (2Set (the_Vertices_of G)) \/ (singletons (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)} ) )