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