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

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

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

then e DJoins v,w,G by A1, Th11;
hence e Joins v,w,G by GLIB_000:16; :: thesis: verum

end;

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

then e DJoins w,v,G by A1, Th11;
hence e Joins v,w,G by GLIB_000:16; :: thesis: verum

end;

end;