let G be _Graph; for W being Walk of G st W is minlength holds
for m, n being natural odd number st m <= n & n <= len W holds
W .cut m,n is minlength
let W be Walk of G; ( W is minlength implies for m, n being natural odd number st m <= n & n <= len W holds
W .cut m,n is minlength )
assume A1:
W is minlength
; for m, n being natural odd number st m <= n & n <= len W holds
W .cut m,n is minlength
let m, n be odd Nat; ( m <= n & n <= len W implies W .cut m,n is minlength )
assume that
A2:
m <= n
and
A3:
n <= len W
; W .cut m,n is minlength
set S = W .cut m,n;
assume
not W .cut m,n is minlength
; contradiction
then consider M being Walk of G such that
A4:
M is_Walk_from (W .cut m,n) .first() ,(W .cut m,n) .last()
and
A5:
len M < len (W .cut m,n)
by Def2;
set R = W .cut 1,m;
A6:
(2 * 0 ) + 1 <= m
by ABIAN:12;
set T = W .cut n,(len W);
A7:
n in NAT
by ORDINAL1:def 13;
then A8:
(W .cut n,(len W)) .first() = W . n
by A3, GLIB_001:38;
set A = (W .cut 1,m) .append M;
A9:
m in NAT
by ORDINAL1:def 13;
A10:
m <= len W
by A2, A3, XXREAL_0:2;
then A11:
(W .cut 1,m) .last() = W . m
by A6, A9, GLIB_001:38;
(W .cut m,n) .first() = W . m
by A2, A3, A9, A7, GLIB_001:38;
then A12:
M .first() = W . m
by A4, GLIB_001:def 23;
then
(len ((W .cut 1,m) .append M)) + 1 = (len (W .cut 1,m)) + (len M)
by A11, GLIB_001:29;
then A13:
(len ((W .cut 1,m) .append M)) + 1 < (len (W .cut 1,m)) + (len (W .cut m,n))
by A5, XREAL_1:10;
set B = ((W .cut 1,m) .append M) .append (W .cut n,(len W));
(W .cut m,n) .last() = W . n
by A2, A3, A9, A7, GLIB_001:38;
then
M .last() = W . n
by A4, GLIB_001:def 23;
then A14:
((W .cut 1,m) .append M) .last() = W . n
by A11, A12, GLIB_001:31;
then A15:
(len (((W .cut 1,m) .append M) .append (W .cut n,(len W)))) + 1 = (len ((W .cut 1,m) .append M)) + (len (W .cut n,(len W)))
by A8, GLIB_001:29;
A16:
(len (W .cut 1,m)) + 1 = m + 1
by A6, A10, A9, GLIB_001:37;
(len (W .cut m,n)) + m = n + 1
by A2, A3, A9, A7, GLIB_001:37;
then
((len ((W .cut 1,m) .append M)) + 1) - 1 < (n + 1) - 1
by A16, A13, XREAL_1:16;
then A17:
(len (((W .cut 1,m) .append M) .append (W .cut n,(len W)))) + 1 < (len (W .cut n,(len W))) + n
by A15, XREAL_1:10;
(len (W .cut n,(len W))) + n = (len W) + 1
by A3, A7, GLIB_001:37;
then A18:
((len (((W .cut 1,m) .append M) .append (W .cut n,(len W)))) + 1) - 1 < ((len W) + 1) - 1
by A17, XREAL_1:16;
(W .cut n,(len W)) .last() = W . (len W)
by A3, A7, GLIB_001:38;
then A19:
(((W .cut 1,m) .append M) .append (W .cut n,(len W))) .last() = W .last()
by A8, A14, GLIB_001:31;
(W .cut 1,m) .first() = W . 1
by A6, A10, A9, GLIB_001:38;
then
((W .cut 1,m) .append M) .first() = W . 1
by A11, A12, GLIB_001:31;
then
(((W .cut 1,m) .append M) .append (W .cut n,(len W))) .first() = W .first()
by A8, A14, GLIB_001:31;
then
((W .cut 1,m) .append M) .append (W .cut n,(len W)) is_Walk_from W .first() ,W .last()
by A19, GLIB_001:def 23;
hence
contradiction
by A1, A18, Def2; verum