:: deftheorem Def1 defines replaceVerticesEdges GLIB_015:def 1 :
for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for b₄ being plain _Graph holds
( b₄ = replaceVerticesEdges (V,E) iff ex S, T being Function of (rng E),(rng V) st
( S = (V * (the_Source_of G)) * (E ") & T = (V * (the_Target_of G)) * (E ") & b₄ = createGraph ((rng V),(rng E),S,T) ) );