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

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

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

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

end;

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

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

end;

end;