let G be _Graph; :: thesis: for e, x, y being object st e Joins x,y,G holds
(G .walkOf (x,e,y)) .vertices() = {x,y}
let e, x, y be object ; :: 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 Th68;
hence (G .walkOf (x,e,y)) .vertices() = {x,y} by FINSEQ_2:127; :: thesis: verum