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:146;

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:36;
A8: (2 * 0) + 1 <= m by ABIAN:12;
then A9: ((len (W .cut (1,m))) + 1) - 1 = (m + 1) - 1 by A2, GLIB_001:36;
A10: (W .cut (n,(len W))) .first() = W . m by A3, A4, GLIB_001:37;
A11: (W .cut (1,m)) .last() = W . m by A2, A8, GLIB_001:37;
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:28;
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:8;
A13: (W .cut (n,(len W))) .last() = W . (len W) by A3, GLIB_001:37;
(W .cut (1,m)) .first() = W . ((2 * 0) + 1) by A2, A8, GLIB_001:37;
then (W .cut (1,m)) .append (W .cut (n,(len W))) is_Walk_from W .first() ,W .last() by A11, A10, A13, GLIB_001:30;
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:36;
A16: (2 * 0) + 1 <= n by ABIAN:12;
then A17: ((len (W .cut (1,n))) + 1) - 1 = (n + 1) - 1 by A3, GLIB_001:36;
A18: (W .cut (m,(len W))) .first() = W . n by A2, A4, GLIB_001:37;
A19: (W .cut (1,n)) .last() = W . n by A3, A16, GLIB_001:37;
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:28;
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:8;
A21: (W .cut (m,(len W))) .last() = W . (len W) by A2, GLIB_001:37;
(W .cut (1,n)) .first() = W . ((2 * 0) + 1) by A3, A16, GLIB_001:37;
then (W .cut (1,n)) .append (W .cut (m,(len W))) is_Walk_from W .first() ,W .last() by A19, A18, A21, GLIB_001:30;
hence contradiction by A1, A20, Def2; :: thesis: verum

end;

end;