theorem Th18: :: GLIB_015:18

for G being _Graph
for V being non empty one-to-one ManySortedSet of the_Vertices_of G
for E being one-to-one ManySortedSet of the_Edges_of G
for W1 being Walk of G ex W2 being Walk of replaceVerticesEdges (V,E) st
( V * (W1 .vertexSeq()) = W2 .vertexSeq() & E * (W1 .edgeSeq()) = W2 .edgeSeq() )