let G be _Graph; :: thesis: for x, e, y being object st e Joins x,y,G holds
len (G .walkOf (x,e,y)) = 3
let x, e, y be object ; :: 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:45; :: thesis: verum