let G be _Graph; :: thesis: for e, x, y being set st e Joins x,y,G holds
( (G .walkOf x,e,y) .first() = x & (G .walkOf x,e,y) .last() = y & G .walkOf x,e,y is_Walk_from x,y )
let e, x, y be set ; :: thesis: ( e Joins x,y,G implies ( (G .walkOf x,e,y) .first() = x & (G .walkOf x,e,y) .last() = y & G .walkOf x,e,y is_Walk_from x,y ) )
set W = G .walkOf x,e,y;
assume e Joins x,y,G ; :: thesis: ( (G .walkOf x,e,y) .first() = x & (G .walkOf x,e,y) .last() = y & G .walkOf x,e,y is_Walk_from x,y )
then A1: G .walkOf x,e,y = <*x,e,y*> by Def5;
hence A2: (G .walkOf x,e,y) .first() = x by FINSEQ_1:62; :: thesis: ( (G .walkOf x,e,y) .last() = y & G .walkOf x,e,y is_Walk_from x,y )
len (G .walkOf x,e,y) = 3 by A1, FINSEQ_1:62;
hence (G .walkOf x,e,y) .last() = y by A1, FINSEQ_1:62; :: thesis: G .walkOf x,e,y is_Walk_from x,y
hence G .walkOf x,e,y is_Walk_from x,y by A2, Def23; :: thesis: verum