let G be _Graph; :: thesis: for e, x, y being set st e Joins x,y,G holds
(G .walkOf x,e,y) .vertices() = {x,y}
let e, x, y be set ; :: thesis: ( e Joins x,y,G implies (G .walkOf x,e,y) .vertices() = {x,y} )
set W = G .walkOf x,e,y;
assume e Joins x,y,G ; :: thesis: (G .walkOf x,e,y) .vertices() = {x,y}
then (G .walkOf x,e,y) .vertexSeq() = <*x,y*> by Th71;
hence (G .walkOf x,e,y) .vertices() = {x,y} by FINSEQ_2:147; :: thesis: verum