let G be _Graph; :: thesis: for W being Walk of G st W is minlength holds
W is Path-like
let W be Walk of G; :: thesis: ( W is minlength implies W is Path-like )
assume A1:
W is minlength
; :: thesis: W is Path-like
assume
not W is Path-like
; :: thesis: contradiction
then consider m, n being odd Element of NAT such that
A2:
( m <= len W & n <= len W )
and
A3:
W . m = W . n
and
A4:
m <> n
by GLIB_001:147;
per cases
( m < n or n < m )
by A4, XXREAL_0:1;
suppose A5:
m < n
;
:: thesis: contradictionset R =
W .cut 1,
m;
set S =
W .cut n,
(len W);
A6:
(2 * 0 ) + 1
<= m
by HEYTING3:1;
then A7:
(
(W .cut 1,m) .first() = W . ((2 * 0 ) + 1) &
(W .cut 1,m) .last() = W . m )
by A2, GLIB_001:38;
A8:
(
(W .cut n,(len W)) .first() = W . m &
(W .cut n,(len W)) .last() = W . (len W) )
by A2, A3, GLIB_001:38;
A9:
((len (W .cut 1,m)) + 1) - 1
= (m + 1) - 1
by A2, A6, GLIB_001:37;
A10:
((len (W .cut n,(len W))) + n) - n = ((len W) + 1) - n
by A2, GLIB_001:37;
set P =
(W .cut 1,m) .append (W .cut n,(len W));
A11:
(W .cut 1,m) .append (W .cut n,(len W)) is_Walk_from W .first() ,
W .last()
by A7, A8, GLIB_001:31;
(len ((W .cut 1,m) .append (W .cut n,(len W)))) + 1
= (len (W .cut 1,m)) + (len (W .cut n,(len W)))
by A7, A8, GLIB_001:29;
then
len ((W .cut 1,m) .append (W .cut n,(len W))) = ((len W) - n) + m
by A9, A10;
then
len ((W .cut 1,m) .append (W .cut n,(len W))) < ((len W) - n) + n
by A5, XREAL_1:10;
hence
contradiction
by A1, A11, Def2;
:: thesis: verum end; suppose A12:
n < m
;
:: thesis: contradictionset R =
W .cut 1,
n;
set S =
W .cut m,
(len W);
A13:
(2 * 0 ) + 1
<= n
by HEYTING3:1;
then A14:
(
(W .cut 1,n) .first() = W . ((2 * 0 ) + 1) &
(W .cut 1,n) .last() = W . n )
by A2, GLIB_001:38;
A15:
(
(W .cut m,(len W)) .first() = W . n &
(W .cut m,(len W)) .last() = W . (len W) )
by A2, A3, GLIB_001:38;
A16:
((len (W .cut 1,n)) + 1) - 1
= (n + 1) - 1
by A2, A13, GLIB_001:37;
A17:
((len (W .cut m,(len W))) + m) - m = ((len W) + 1) - m
by A2, GLIB_001:37;
set P =
(W .cut 1,n) .append (W .cut m,(len W));
A18:
(W .cut 1,n) .append (W .cut m,(len W)) is_Walk_from W .first() ,
W .last()
by A14, A15, GLIB_001:31;
(len ((W .cut 1,n) .append (W .cut m,(len W)))) + 1
= (len (W .cut 1,n)) + (len (W .cut m,(len W)))
by A14, A15, GLIB_001:29;
then
len ((W .cut 1,n) .append (W .cut m,(len W))) = ((len W) - m) + n
by A16, A17;
then
len ((W .cut 1,n) .append (W .cut m,(len W))) < ((len W) - m) + m
by A12, XREAL_1:10;
hence
contradiction
by A1, A18, Def2;
:: thesis: verum end;