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 DJoins v,w,G holds
e DJoins 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 DJoins v,w,G holds
e DJoins V . v,V . w, replaceVertices V
let e, v, w be object ; :: thesis: ( e DJoins v,w,G implies e DJoins V . v,V . w, replaceVertices V )
assume A1: e DJoins v,w,G ; :: thesis: e DJoins V . v,V . w, replaceVertices V
(id (the_Edges_of G)) . e DJoins V . v,V . w, replaceVertices V by A1, Th4;
hence e DJoins V . v,V . w, replaceVertices V by A1, FUNCT_1:18, GLIB_000:def 14; :: thesis: verum