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 + 2 < n & n <= len W holds
for e being set holds not e Joins W . m,W . n,G
let P be Walk of G; :: thesis: ( P is minlength implies for m, n being natural odd number st m + 2 < n & n <= len P holds
for e being set holds not e Joins P . m,P . n,G )
assume A1: P is minlength ; :: thesis: for m, n being natural odd number st m + 2 < n & n <= len P holds
for e being set 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 set holds not e Joins P . m,P . n,G )
assume that
A2: m + 2 < n and
A3: n <= len P ; :: thesis: for e being set holds not e Joins P . m,P . n,G
A4: ((len P) - n) + (m + 2) < ((len P) - n) + n by A2, XREAL_1:10;
m + 0 <= m + 2 by XREAL_1:9;
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 13;
then A7: (P .cut n,(len P)) .last() = P .last() by A3, GLIB_001:38;
set P1 = P .cut 1,m;
let e be set ; :: 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 13;
then A11: (len (P .cut 1,m)) + 1 = m + 1 by A9, A5, GLIB_001:37;
A12: (P .cut 1,m) .last() = P . m by A10, A9, A5, GLIB_001:38;
then A13: ((P .cut 1,m) .addEdge e) .last() = P . n by A8, GLIB_001:64;
(P .cut 1,m) .first() = P .first() by A10, A9, A5, GLIB_001:38;
then A14: ((P .cut 1,m) .addEdge e) .first() = P .first() by A8, A12, GLIB_001:64;
(P .cut n,(len P)) .first() = P . n by A3, A6, GLIB_001:38;
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:31;
(P .cut n,(len P)) .first() = P . n by A3, A6, GLIB_001:38;
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:29;
(P .cut 1,m) .last() = P . m by A10, A9, A5, GLIB_001:38;
then A17: len ((P .cut 1,m) .addEdge e) = m + 2 by A8, A11, GLIB_001:65;
(len (P .cut n,(len P))) + n = (len P) + 1 by A3, A6, GLIB_001:37;
hence contradiction by A1, A17, A15, A16, A4, Def2; :: thesis: verum