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 Joins v,w,G holds
E . e Joins 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 Joins v,w,G holds
E . e Joins v,w, replaceEdges E
let e, v, w be object ; :: thesis: ( e Joins v,w,G implies E . e Joins v,w, replaceEdges E )
assume e Joins v,w,G ; :: thesis: E . e Joins v,w, replaceEdges E

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 . e Joins v,w, replaceEdges E

then E . e DJoins v,w, replaceEdges E by Th6;
hence E . e Joins v,w, replaceEdges E by GLIB_000:16; :: thesis: verum

end;

suppose e DJoins w,v,G ; :: thesis: E . e Joins v,w, replaceEdges E

then E . e DJoins w,v, replaceEdges E by Th6;
hence E . e Joins v,w, replaceEdges E by GLIB_000:16; :: thesis: verum

end;

end;