let G be _Graph; :: thesis: for W being Walk of G st W is minlength holds
W is Path-like
let W be Walk of G; :: thesis: ( W is minlength implies W is Path-like )
assume A1: W is minlength ; :: thesis: W is Path-like
assume not W is Path-like ; :: thesis: contradiction
then consider m, n being odd Element of NAT such that
A2: m <= len W and
A3: n <= len W and
A4: W . m = W . n and
A5: m <> n by GLIB_001:147;

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

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

set R = W .cut 1,m;
set S = W .cut n,(len W);
set P = (W .cut 1,m) .append (W .cut n,(len W));
A7: ((len (W .cut n,(len W))) + n) - n = ((len W) + 1) - n by A3, GLIB_001:37;
A8: (2 * 0 ) + 1 <= m by ABIAN:12;
then A9: ((len (W .cut 1,m)) + 1) - 1 = (m + 1) - 1 by A2, GLIB_001:37;
A10: (W .cut n,(len W)) .first() = W . m by A3, A4, GLIB_001:38;
A11: (W .cut 1,m) .last() = W . m by A2, A8, GLIB_001:38;
then (len ((W .cut 1,m) .append (W .cut n,(len W)))) + 1 = (len (W .cut 1,m)) + (len (W .cut n,(len W))) by A10, GLIB_001:29;
then len ((W .cut 1,m) .append (W .cut n,(len W))) = ((len W) - n) + m by A9, A7;
then A12: len ((W .cut 1,m) .append (W .cut n,(len W))) < ((len W) - n) + n by A6, XREAL_1:10;
A13: (W .cut n,(len W)) .last() = W . (len W) by A3, GLIB_001:38;
(W .cut 1,m) .first() = W . ((2 * 0 ) + 1) by A2, A8, GLIB_001:38;
then (W .cut 1,m) .append (W .cut n,(len W)) is_Walk_from W .first() ,W .last() by A11, A10, A13, GLIB_001:31;
hence contradiction by A1, A12, Def2; :: thesis: verum

end;

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

set R = W .cut 1,n;
set S = W .cut m,(len W);
set P = (W .cut 1,n) .append (W .cut m,(len W));
A15: ((len (W .cut m,(len W))) + m) - m = ((len W) + 1) - m by A2, GLIB_001:37;
A16: (2 * 0 ) + 1 <= n by ABIAN:12;
then A17: ((len (W .cut 1,n)) + 1) - 1 = (n + 1) - 1 by A3, GLIB_001:37;
A18: (W .cut m,(len W)) .first() = W . n by A2, A4, GLIB_001:38;
A19: (W .cut 1,n) .last() = W . n by A3, A16, GLIB_001:38;
then (len ((W .cut 1,n) .append (W .cut m,(len W)))) + 1 = (len (W .cut 1,n)) + (len (W .cut m,(len W))) by A18, GLIB_001:29;
then len ((W .cut 1,n) .append (W .cut m,(len W))) = ((len W) - m) + n by A17, A15;
then A20: len ((W .cut 1,n) .append (W .cut m,(len W))) < ((len W) - m) + m by A14, XREAL_1:10;
A21: (W .cut m,(len W)) .last() = W . (len W) by A2, GLIB_001:38;
(W .cut 1,n) .first() = W . ((2 * 0 ) + 1) by A3, A16, GLIB_001:38;
then (W .cut 1,n) .append (W .cut m,(len W)) is_Walk_from W .first() ,W .last() by A19, A18, A21, GLIB_001:31;
hence contradiction by A1, A20, Def2; :: thesis: verum

end;

end;