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

now

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 (choose (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