let G be _Graph; :: thesis: for W being Walk of G st not W is closed & W is Path-like holds
W is vertex-distinct
let W be Walk of G; :: thesis: ( not W is closed & W is Path-like implies W is vertex-distinct )
assume that
A1: not W is closed and
A2: W is Path-like ; :: thesis: W is vertex-distinct

now

let m, n be odd Element of NAT ; :: thesis: ( m <= len W & n <= len W & W . m = W . n implies not m <> n )
assume that
A3: m <= len W and
A4: n <= len W and
A5: W . m = W . n ; :: thesis: not m <> n
assume A6: m <> n ; :: thesis: contradiction

per cases ( m < n or m > n ) by A6, XXREAL_0:1;

suppose A7: m < n ; :: thesis: contradiction

then A8: W . n = W .last() by A2, A4, A5, GLIB_001:def 28;
W . m = W .first() by A2, A4, A5, A7, GLIB_001:def 28;
hence contradiction by A1, A5, A8, GLIB_001:def 24; :: thesis: verum

end;

suppose A9: m > n ; :: thesis: contradiction

then A10: W . n = W .first() by A2, A3, A5, GLIB_001:def 28;
W . m = W .last() by A2, A3, A5, A9, GLIB_001:def 28;
hence contradiction by A1, A5, A10, GLIB_001:def 24; :: thesis: verum

end;

end;

end;

hence W is vertex-distinct by GLIB_001:def 29; :: thesis: verum