let W be Walk of G; :: thesis: ( W is vertex-distinct implies W is Path-like )
assume W is vertex-distinct ; :: thesis: W is Path-like
then for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds
m = n by Def29;
hence W is Path-like by Lm66; :: thesis: verum