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

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

( 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

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;
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;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

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