set W = G .walkOf (x,e,y);

now :: thesis: G .walkOf (x,e,y) is Path-like

per cases ( e Joins x,y,G or not e Joins x,y,G ) ;

suppose e Joins x,y,G ; :: thesis: G .walkOf (x,e,y) is Path-like

hence G .walkOf (x,e,y) is Path-like by Lm62; :: thesis: verum

end;

suppose not e Joins x,y,G ; :: thesis: G .walkOf (x,e,y) is Path-like

then G .walkOf (x,e,y) = G .walkOf the Element of the_Vertices_of G by Def5;
hence G .walkOf (x,e,y) is Path-like ; :: thesis: verum

end;

end;

end;

hence G .walkOf (x,e,y) is Path-like ; :: thesis: verum