let G be _Graph; :: thesis: for E being one-to-one ManySortedSet of the_Edges_of G
for e, v, w being object st e DJoins v,w,G holds
E . e DJoins v,w, replaceEdges E
let E be one-to-one ManySortedSet of the_Edges_of G; :: thesis: for e, v, w being object st e DJoins v,w,G holds
E . e DJoins v,w, replaceEdges E
let e, v, w be object ; :: thesis: ( e DJoins v,w,G implies E . e DJoins v,w, replaceEdges E )
assume A1: e DJoins v,w,G ; :: thesis: E . e DJoins v,w, replaceEdges E
then e Joins v,w,G by GLIB_000:16;
then A2: ( v in the_Vertices_of G & w in the_Vertices_of G ) by GLIB_000:13;
E . e DJoins (id (the_Vertices_of G)) . v,(id (the_Vertices_of G)) . w, replaceEdges E by A1, Th4;
then E . e DJoins v,(id (the_Vertices_of G)) . w, replaceEdges E by A2, FUNCT_1:18;
hence E . e DJoins v,w, replaceEdges E by A2, FUNCT_1:18; :: thesis: verum