theorem :: GLIB_015:8

for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for e, v, w being object st e Joins v,w,G holds
e Joins V . v,V . w, replaceVertices V