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