let G be _Graph; :: thesis: for x, e, y being object 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 x, e, y be object ; :: 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 ; :: 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:45;
hence (G .walkOf (x,e,y)) .last() = y by A1; :: thesis: G .walkOf (x,e,y) is_Walk_from x,y
hence G .walkOf (x,e,y) is_Walk_from x,y by A2; :: thesis: verum