let G be _Graph; :: thesis: for W being Walk of G st W is minlength holds
for m, n being odd Nat st m + 2 < n & n <= len W holds
for e being object holds not e Joins W . m,W . n,G

let P be Walk of G; :: thesis: ( P is minlength implies for m, n being odd Nat st m + 2 < n & n <= len P holds
for e being object holds not e Joins P . m,P . n,G )

assume A1: P is minlength ; :: thesis: for m, n being odd Nat st m + 2 < n & n <= len P holds
for e being object holds not e Joins P . m,P . n,G

let m, n be odd Nat; :: thesis: ( m + 2 < n & n <= len P implies for e being object holds not e Joins P . m,P . n,G )
assume that
A2: m + 2 < n and
A3: n <= len P ; :: thesis: for e being object holds not e Joins P . m,P . n,G
A4: ((len P) - n) + (m + 2) < ((len P) - n) + n by ;
m + 0 <= m + 2 by XREAL_1:7;
then m <= n by ;
then A5: m <= len P by ;
set P3 = P .cut (n,(len P));
A6: n in NAT by ORDINAL1:def 12;
then A7: (P .cut (n,(len P))) .last() = P .last() by ;
set P1 = P .cut (1,m);
let e be object ; :: thesis: not e Joins P . m,P . n,G
assume A8: e Joins P . m,P . n,G ; :: thesis: contradiction
set P2 = (P .cut (1,m)) .addEdge e;
set P4 = ((P .cut (1,m)) .addEdge e) .append (P .cut (n,(len P)));
A9: (2 * 0) + 1 <= m by ABIAN:12;
A10: m in NAT by ORDINAL1:def 12;
then A11: (len (P .cut (1,m))) + 1 = m + 1 by ;
A12: (P .cut (1,m)) .last() = P . m by ;
then A13: ((P .cut (1,m)) .addEdge e) .last() = P . n by ;
(P .cut (1,m)) .first() = P .first() by ;
then A14: ((P .cut (1,m)) .addEdge e) .first() = P .first() by ;
(P .cut (n,(len P))) .first() = P . n by ;
then A15: ((P .cut (1,m)) .addEdge e) .append (P .cut (n,(len P))) is_Walk_from P .first() ,P .last() by ;
(P .cut (n,(len P))) .first() = P . n by ;
then A16: (len (((P .cut (1,m)) .addEdge e) .append (P .cut (n,(len P))))) + 1 = (len ((P .cut (1,m)) .addEdge e)) + (len (P .cut (n,(len P)))) by ;
(P .cut (1,m)) .last() = P . m by ;
then A17: len ((P .cut (1,m)) .addEdge e) = m + 2 by ;
(len (P .cut (n,(len P)))) + n = (len P) + 1 by ;
hence contradiction by A1, A17, A15, A16, A4; :: thesis: verum