let G be _Graph; 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; ( 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
; 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; ( 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
; 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 ; not e Joins P . m,P . n,G
assume A8:
e Joins P . m,P . n,G
; 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; verum