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