let G be _Graph; :: thesis: for W being Walk of G
for x, y being set st W is_Walk_from x,y holds
( x is Vertex of G & y is Vertex of G )
let W be Walk of G; :: thesis: for x, y being set st W is_Walk_from x,y holds
( x is Vertex of G & y is Vertex of G )
let x, y be set ; :: thesis: ( W is_Walk_from x,y implies ( x is Vertex of G & y is Vertex of G ) )
assume A1: W is_Walk_from x,y ; :: thesis: ( x is Vertex of G & y is Vertex of G )
then A2: W .last() = y by Def23;
W .first() = x by A1, Def23;
hence ( x is Vertex of G & y is Vertex of G ) by A2; :: thesis: verum