let G be _Graph; :: thesis: for W being Walk of G st W is minlength holds
for m, n being odd Nat st m <= n & n <= len W holds
W .cut (m,n) is minlength
let W be Walk of G; :: thesis: ( W is minlength implies for m, n being odd Nat st m <= n & n <= len W holds
W .cut (m,n) is minlength )
assume A1: W is minlength ; :: thesis: for m, n being odd Nat st m <= n & n <= len W holds
W .cut (m,n) is minlength
let m, n be odd Nat; :: thesis: ( m <= n & n <= len W implies W .cut (m,n) is minlength )
assume that
A2: m <= n and
A3: n <= len W ; :: thesis: W .cut (m,n) is minlength
set S = W .cut (m,n);
assume not W .cut (m,n) is minlength ; :: thesis: contradiction
then consider M being Walk of G such that
A4: M is_Walk_from (W .cut (m,n)) .first() ,(W .cut (m,n)) .last() and
A5: len M < len (W .cut (m,n)) ;
set R = W .cut (1,m);
A6: (2 * 0) + 1 <= m by ABIAN:12;
set T = W .cut (n,(len W));
A7: n in NAT by ORDINAL1:def 12;
then A8: (W .cut (n,(len W))) .first() = W . n by A3, GLIB_001:37;
set A = (W .cut (1,m)) .append M;
A9: m in NAT by ORDINAL1:def 12;
A10: m <= len W by A2, A3, XXREAL_0:2;
then A11: (W .cut (1,m)) .last() = W . m by A6, A9, GLIB_001:37;
(W .cut (m,n)) .first() = W . m by A2, A3, A9, A7, GLIB_001:37;
then A12: M .first() = W . m by A4;
then (len ((W .cut (1,m)) .append M)) + 1 = (len (W .cut (1,m))) + (len M) by A11, GLIB_001:28;
then A13: (len ((W .cut (1,m)) .append M)) + 1 < (len (W .cut (1,m))) + (len (W .cut (m,n))) by A5, XREAL_1:8;
set B = ((W .cut (1,m)) .append M) .append (W .cut (n,(len W)));
(W .cut (m,n)) .last() = W . n by A2, A3, A9, A7, GLIB_001:37;
then M .last() = W . n by A4;
then A14: ((W .cut (1,m)) .append M) .last() = W . n by A11, A12, GLIB_001:30;
then A15: (len (((W .cut (1,m)) .append M) .append (W .cut (n,(len W))))) + 1 = (len ((W .cut (1,m)) .append M)) + (len (W .cut (n,(len W)))) by A8, GLIB_001:28;
A16: (len (W .cut (1,m))) + 1 = m + 1 by A6, A10, A9, GLIB_001:36;
(len (W .cut (m,n))) + m = n + 1 by A2, A3, A9, A7, GLIB_001:36;
then ((len ((W .cut (1,m)) .append M)) + 1) - 1 < (n + 1) - 1 by A16, A13, XREAL_1:14;
then A17: (len (((W .cut (1,m)) .append M) .append (W .cut (n,(len W))))) + 1 < (len (W .cut (n,(len W)))) + n by A15, XREAL_1:8;
(len (W .cut (n,(len W)))) + n = (len W) + 1 by A3, A7, GLIB_001:36;
then A18: ((len (((W .cut (1,m)) .append M) .append (W .cut (n,(len W))))) + 1) - 1 < ((len W) + 1) - 1 by A17, XREAL_1:14;
(W .cut (n,(len W))) .last() = W . (len W) by A3, A7, GLIB_001:37;
then A19: (((W .cut (1,m)) .append M) .append (W .cut (n,(len W)))) .last() = W .last() by A8, A14, GLIB_001:30;
(W .cut (1,m)) .first() = W . 1 by A6, A10, A9, GLIB_001:37;
then ((W .cut (1,m)) .append M) .first() = W . 1 by A11, A12, GLIB_001:30;
then (((W .cut (1,m)) .append M) .append (W .cut (n,(len W)))) .first() = W .first() by A8, A14, GLIB_001:30;
then ((W .cut (1,m)) .append M) .append (W .cut (n,(len W))) is_Walk_from W .first() ,W .last() by A19;
hence contradiction by A1, A18; :: thesis: verum