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() } ;
set T = the Path-like Subwalk of W;
A1: the Path-like Subwalk of W .last() = W .last() by GLIB_001:161;
the Path-like Subwalk of W .first() = W .first() by GLIB_001:161;
then the Path-like Subwalk of W is_Walk_from W .first() ,W .last() by A1;
then A2: len the Path-like Subwalk of W 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 object ; :: 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;
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;
set T = the Path-like Subwalk of W2;
A8: the Path-like Subwalk of W2 .first() = W2 .first() by GLIB_001:161;
A9: the Path-like Subwalk of W2 .last() = W2 .last() by GLIB_001:161;
A10: P .last() = W .last() by A4;
P .first() = W2 .first() by A6;
then the Path-like Subwalk of W2 is_Walk_from W .first() ,W .last() by A7, A5, A10, A8, A9;
then len the Path-like Subwalk of W2 in X ;
then A11: len P <= len the Path-like Subwalk of W2 by A3, XXREAL_2:def 7;
len the Path-like Subwalk of W2 <= len W2 by GLIB_001:162;
hence len W2 >= len P by A11, XXREAL_0:2; :: thesis: verum