let G be _Graph; :: thesis: 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
let V be non empty one-to-one ManySortedSet of the_Vertices_of G; :: thesis: for e, v, w being object st e Joins v,w,G holds
e Joins V . v,V . w, replaceVertices V
let e, v, w be object ; :: thesis: ( e Joins v,w,G implies e Joins V . v,V . w, replaceVertices V )
assume e Joins v,w,G ; :: thesis: e Joins V . v,V . w, replaceVertices V

per cases then ( e DJoins v,w,G or e DJoins w,v,G ) by GLIB_000:16;

suppose e DJoins v,w,G ; :: thesis: e Joins V . v,V . w, replaceVertices V

then e DJoins V . v,V . w, replaceVertices V by Th5;
hence e Joins V . v,V . w, replaceVertices V by GLIB_000:16; :: thesis: verum

end;

suppose e DJoins w,v,G ; :: thesis: e Joins V . v,V . w, replaceVertices V

then e DJoins V . w,V . v, replaceVertices V by Th5;
hence e Joins V . v,V . w, replaceVertices V by GLIB_000:16; :: thesis: verum

end;

end;