theorem Th2: :: GLIB_015:2

for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G holds
( the_Vertices_of (replaceVertices V) = rng V & the_Edges_of (replaceVertices V) = the_Edges_of G & the_Source_of (replaceVertices V) = V * (the_Source_of G) & the_Target_of (replaceVertices V) = V * (the_Target_of G) )