let G be _Graph; :: thesis: for W being Walk of G ex P being Path of G st
( P is_Walk_from W .first() ,W .last() & P is minlength )
let W be Walk of G; :: thesis: ex P being Path of G st
( P is_Walk_from W .first() ,W .last() & P is minlength )
set X = { (len P) where P is Path of G : P is_Walk_from W .first() ,W .last() } ;
consider T being Path-like Subwalk of W;
A1: T .last() = W .last() by GLIB_001:162;
T .first() = W .first() by GLIB_001:162;
then T is_Walk_from W .first() ,W .last() by A1, GLIB_001:def 23;
then A2: len T in { (len P) where P is Path of G : P is_Walk_from W .first() ,W .last() } ;
{ (len P) where P is Path of G : P is_Walk_from W .first() ,W .last() } c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (len P) where P is Path of G : P is_Walk_from W .first() ,W .last() } or x in NAT )
assume x in { (len P) where P is Path of G : P is_Walk_from W .first() ,W .last() } ; :: thesis: x in NAT
then ex P being Path of G st
( x = len P & P is_Walk_from W .first() ,W .last() ) ;
hence x in NAT ; :: thesis: verum

end;

then reconsider X = { (len P) where P is Path of G : P is_Walk_from W .first() ,W .last() } as non empty Subset of NAT by A2;
min X in X by XXREAL_2:def 7;
then consider P being Path of G such that
A3: len P = min X and
A4: P is_Walk_from W .first() ,W .last() ;
A5: P .first() = W .first() by A4, GLIB_001:def 23;
take P ; :: thesis: ( P is_Walk_from W .first() ,W .last() & P is minlength )
thus P is_Walk_from W .first() ,W .last() by A4; :: thesis: P is minlength
let W2 be Walk of G; :: according to CHORD:def 2 :: thesis: ( W2 is_Walk_from P .first() ,P .last() implies len W2 >= len P )
assume A6: W2 is_Walk_from P .first() ,P .last() ; :: thesis: len W2 >= len P
A7: P .last() = W2 .last() by A6, GLIB_001:def 23;
consider T being Path-like Subwalk of W2;
A8: T .first() = W2 .first() by GLIB_001:162;
A9: T .last() = W2 .last() by GLIB_001:162;
A10: P .last() = W .last() by A4, GLIB_001:def 23;
P .first() = W2 .first() by A6, GLIB_001:def 23;
then T is_Walk_from W .first() ,W .last() by A7, A5, A10, A8, A9, GLIB_001:def 23;
then len T in X ;
then A11: len P <= len T by A3, XXREAL_2:def 7;
len T <= len W2 by GLIB_001:163;
hence len W2 >= len P by A11, XXREAL_0:2; :: thesis: verum