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

now :: thesis: for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds
not m <> n

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;
W . m = W .first() by A2, A4, A5, A7;
hence contradiction by A1, A5, A8; :: thesis: verum

end;

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

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

end;

end;

end;

hence W is vertex-distinct ; :: thesis: verum