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 ;
set A = (W .cut (1,m)) .append M;
A9: m in NAT by ORDINAL1:def 12;
A10: m <= len W by ;
then A11: (W .cut (1,m)) .last() = W . m by ;
(W .cut (m,n)) .first() = W . m by ;
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 ;
then A13: (len ((W .cut (1,m)) .append M)) + 1 < (len (W .cut (1,m))) + (len (W .cut (m,n))) by ;
set B = ((W .cut (1,m)) .append M) .append (W .cut (n,(len W)));
(W .cut (m,n)) .last() = W . n by ;
then M .last() = W . n by A4;
then A14: ((W .cut (1,m)) .append M) .last() = W . n by ;
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 ;
A16: (len (W .cut (1,m))) + 1 = m + 1 by ;
(len (W .cut (m,n))) + m = n + 1 by ;
then ((len ((W .cut (1,m)) .append M)) + 1) - 1 < (n + 1) - 1 by ;
then A17: (len (((W .cut (1,m)) .append M) .append (W .cut (n,(len W))))) + 1 < (len (W .cut (n,(len W)))) + n by ;
(len (W .cut (n,(len W)))) + n = (len W) + 1 by ;
then A18: ((len (((W .cut (1,m)) .append M) .append (W .cut (n,(len W))))) + 1) - 1 < ((len W) + 1) - 1 by ;
(W .cut (n,(len W))) .last() = W . (len W) by ;
then A19: (((W .cut (1,m)) .append M) .append (W .cut (n,(len W)))) .last() = W .last() by ;
(W .cut (1,m)) .first() = W . 1 by ;
then ((W .cut (1,m)) .append M) .first() = W . 1 by ;
then (((W .cut (1,m)) .append M) .append (W .cut (n,(len W)))) .first() = W .first() by ;
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