theorem Th5: :: GLIB_013:5

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