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 that

A1: W is minlength and

A2: not W is Path-like ; :: thesis: contradiction

set s = the Path-like Subwalk of W;

the Path-like Subwalk of W is_Walk_from W .first() ,W .last() by GLIB_001:def 32;

then A3: len W <= len the Path-like Subwalk of W by A1;

len the Path-like Subwalk of W <= len W by GLIB_001:162;

hence contradiction by A2, A3, Th35, XXREAL_0:1; :: thesis: verum

W is Path-like

let W be Walk of G; :: thesis: ( W is minlength implies W is Path-like )

assume that

A1: W is minlength and

A2: not W is Path-like ; :: thesis: contradiction

set s = the Path-like Subwalk of W;

the Path-like Subwalk of W is_Walk_from W .first() ,W .last() by GLIB_001:def 32;

then A3: len W <= len the Path-like Subwalk of W by A1;

len the Path-like Subwalk of W <= len W by GLIB_001:162;

hence contradiction by A2, A3, Th35, XXREAL_0:1; :: thesis: verum