:: deftheorem defines replaceVertices GLIB_015:def 2 :
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G holds replaceVertices V = replaceVerticesEdges (V,(id (the_Edges_of G)));