let G be _Graph; :: thesis: for W being Walk of G st W is minlength holds
for m, n being natural odd number 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 natural odd number st m <= n & n <= len W holds
W .cut m,n is minlength )
assume A1: W is minlength ; :: thesis: for m, n being natural odd number 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 A2: ( m <= n & n <= len W ) ; :: thesis: W .cut m,n is minlength
A3: ( (2 * 0 ) + 1 <= m & 1 <= n & m <= len W ) by A2, HEYTING3:1, XXREAL_0:2;
set R = W .cut 1,m;
set S = W .cut m,n;
set T = W .cut n,(len W);
A4: ( m in NAT & n in NAT ) by ORDINAL1:def 13;
then A5: (W .cut 1,m) .first() = W . 1 by A3, GLIB_001:38;
A6: (W .cut 1,m) .last() = W . m by A3, A4, GLIB_001:38;
A7: (len (W .cut 1,m)) + 1 = m + 1 by A3, A4, GLIB_001:37;
A8: (W .cut m,n) .first() = W . m by A2, A4, GLIB_001:38;
A9: (W .cut m,n) .last() = W . n by A2, A4, GLIB_001:38;
A10: (len (W .cut m,n)) + m = n + 1 by A2, A4, GLIB_001:37;
A11: (W .cut n,(len W)) .first() = W . n by A2, A4, GLIB_001:38;
A12: (W .cut n,(len W)) .last() = W . (len W) by A2, A4, GLIB_001:38;
A13: (len (W .cut n,(len W))) + n = (len W) + 1 by A2, A4, GLIB_001:37;
assume not W .cut m,n is minlength ; :: thesis: contradiction
then consider M being Walk of G such that
A14: M is_Walk_from (W .cut m,n) .first() ,(W .cut m,n) .last() and
A15: len M < len (W .cut m,n) by Def2;
A16: M .first() = W . m by A8, A14, GLIB_001:def 23;
A17: M .last() = W . n by A9, A14, GLIB_001:def 23;
set A = (W .cut 1,m) .append M;
A18: ((W .cut 1,m) .append M) .first() = W . 1 by A5, A6, A16, GLIB_001:31;
A19: ((W .cut 1,m) .append M) .last() = W . n by A6, A16, A17, GLIB_001:31;
(len ((W .cut 1,m) .append M)) + 1 = (len (W .cut 1,m)) + (len M) by A6, A16, GLIB_001:29;
then (len ((W .cut 1,m) .append M)) + 1 < (len (W .cut 1,m)) + (len (W .cut m,n)) by A15, XREAL_1:10;
then A20: ((len ((W .cut 1,m) .append M)) + 1) - 1 < (n + 1) - 1 by A7, A10, XREAL_1:16;
set B = ((W .cut 1,m) .append M) .append (W .cut n,(len W));
A21: (((W .cut 1,m) .append M) .append (W .cut n,(len W))) .first() = W .first() by A11, A18, A19, GLIB_001:31;
A22: (((W .cut 1,m) .append M) .append (W .cut n,(len W))) .last() = W .last() by A11, A12, A19, GLIB_001:31;
(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 A11, A19, GLIB_001:29;
then (len (((W .cut 1,m) .append M) .append (W .cut n,(len W)))) + 1 < (len (W .cut n,(len W))) + n by A20, XREAL_1:10;
then A23: ((len (((W .cut 1,m) .append M) .append (W .cut n,(len W)))) + 1) - 1 < ((len W) + 1) - 1 by A13, XREAL_1:16;
((W .cut 1,m) .append M) .append (W .cut n,(len W)) is_Walk_from W .first() ,W .last() by A21, A22, GLIB_001:def 23;
hence contradiction by A1, A23, Def2; :: thesis: verum