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 v in dom V & w in dom V & e DJoins V . v,V . w, replaceVertices V holds
e DJoins v,w,G
let V be non empty one-to-one ManySortedSet of the_Vertices_of G; :: thesis: for e, v, w being object st v in dom V & w in dom V & e DJoins V . v,V . w, replaceVertices V holds
e DJoins v,w,G
let e, v, w be object ; :: thesis: ( v in dom V & w in dom V & e DJoins V . v,V . w, replaceVertices V implies e DJoins v,w,G )
assume A1: ( v in dom V & w in dom V & e DJoins V . v,V . w, replaceVertices V ) ; :: thesis: e DJoins v,w,G
then e in the_Edges_of (replaceVertices V) by GLIB_000:def 14;
then A2: e in the_Edges_of G by Th2;
then A3: e in dom (id (the_Edges_of G)) ;
(id (the_Edges_of G)) . e = e by A2, FUNCT_1:18;
hence e DJoins v,w,G by A1, A3, Th10; :: thesis: verum