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;
( T .first() = W .first() & T .last() = W .last() ) by GLIB_001:162;
then T is_Walk_from W .first() ,W .last() by GLIB_001:def 23;
then A1: 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 A1;
min X in X by XXREAL_2:def 7;
then consider P being Path of G such that
A2: len P = min X and
A3: P is_Walk_from W .first() ,W .last() ;
take P ; :: thesis: ( P is_Walk_from W .first() ,W .last() & P is minlength )
thus P is_Walk_from W .first() ,W .last() by A3; :: 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 A4: W2 is_Walk_from P .first() ,P .last() ; :: thesis: len W2 >= len P
consider T being Path-like Subwalk of W2;
A5: len T <= len W2 by GLIB_001:163;
A6: ( P .first() = W2 .first() & P .last() = W2 .last() ) by A4, GLIB_001:def 23;
A7: ( P .first() = W .first() & P .last() = W .last() ) by A3, GLIB_001:def 23;
( T .first() = W2 .first() & T .last() = W2 .last() ) by GLIB_001:162;
then T is_Walk_from W .first() ,W .last() by A6, A7, GLIB_001:def 23;
then len T in X ;
then len P <= len T by A2, XXREAL_2:def 7;
hence len P <= len W2 by A5, XXREAL_0:2; :: thesis: verum