theorem Th11: :: GLIB_015:11

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 v in dom V & w in dom V & e DJoins V . v,V . w, replaceVertices V holds
e DJoins v,w,G