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

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