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 DJoins v,w, replaceEdges E holds
e DJoins 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 DJoins v,w, replaceEdges E holds
e DJoins v,w,G
let e, v, w be object ; :: thesis: ( e in dom E & E . e DJoins v,w, replaceEdges E implies e DJoins v,w,G )
assume A1: ( e in dom E & E . e DJoins v,w, replaceEdges E ) ; :: thesis: e DJoins v,w,G
then E . e Joins v,w, replaceEdges E by GLIB_000:16;
then ( v in the_Vertices_of (replaceEdges E) & w in the_Vertices_of (replaceEdges E) ) by GLIB_000:13;
then A2: ( v in the_Vertices_of G & w in the_Vertices_of G ) by Th3;
then A3: ( v in dom (id (the_Vertices_of G)) & w in dom (id (the_Vertices_of G)) ) ;
( (id (the_Vertices_of G)) . v = v & (id (the_Vertices_of G)) . w = w ) by A2, FUNCT_1:18;
hence e DJoins v,w,G by A1, A3, Th10; :: thesis: verum