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 A2, XREAL_1:8;

m + 0 <= m + 2 by XREAL_1:7;

then m <= n by A2, XXREAL_0:2;

then A5: m <= len P by A3, XXREAL_0:2;

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 A3, GLIB_001:37;

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 A9, A5, GLIB_001:36;

A12: (P .cut (1,m)) .last() = P . m by A10, A9, A5, GLIB_001:37;

then A13: ((P .cut (1,m)) .addEdge e) .last() = P . n by A8, GLIB_001:63;

(P .cut (1,m)) .first() = P .first() by A10, A9, A5, GLIB_001:37;

then A14: ((P .cut (1,m)) .addEdge e) .first() = P .first() by A8, A12, GLIB_001:63;

(P .cut (n,(len P))) .first() = P . n by A3, A6, GLIB_001:37;

then A15: ((P .cut (1,m)) .addEdge e) .append (P .cut (n,(len P))) is_Walk_from P .first() ,P .last() by A14, A13, A7, GLIB_001:30;

(P .cut (n,(len P))) .first() = P . n by A3, A6, GLIB_001:37;

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 A13, GLIB_001:28;

(P .cut (1,m)) .last() = P . m by A10, A9, A5, GLIB_001:37;

then A17: len ((P .cut (1,m)) .addEdge e) = m + 2 by A8, A11, GLIB_001:64;

(len (P .cut (n,(len P)))) + n = (len P) + 1 by A3, A6, GLIB_001:36;

hence contradiction by A1, A17, A15, A16, A4; :: thesis: verum

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 A2, XREAL_1:8;

m + 0 <= m + 2 by XREAL_1:7;

then m <= n by A2, XXREAL_0:2;

then A5: m <= len P by A3, XXREAL_0:2;

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 A3, GLIB_001:37;

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 A9, A5, GLIB_001:36;

A12: (P .cut (1,m)) .last() = P . m by A10, A9, A5, GLIB_001:37;

then A13: ((P .cut (1,m)) .addEdge e) .last() = P . n by A8, GLIB_001:63;

(P .cut (1,m)) .first() = P .first() by A10, A9, A5, GLIB_001:37;

then A14: ((P .cut (1,m)) .addEdge e) .first() = P .first() by A8, A12, GLIB_001:63;

(P .cut (n,(len P))) .first() = P . n by A3, A6, GLIB_001:37;

then A15: ((P .cut (1,m)) .addEdge e) .append (P .cut (n,(len P))) is_Walk_from P .first() ,P .last() by A14, A13, A7, GLIB_001:30;

(P .cut (n,(len P))) .first() = P . n by A3, A6, GLIB_001:37;

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 A13, GLIB_001:28;

(P .cut (1,m)) .last() = P . m by A10, A9, A5, GLIB_001:37;

then A17: len ((P .cut (1,m)) .addEdge e) = m + 2 by A8, A11, GLIB_001:64;

(len (P .cut (n,(len P)))) + n = (len P) + 1 by A3, A6, GLIB_001:36;

hence contradiction by A1, A17, A15, A16, A4; :: thesis: verum