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
consider s being Path-like Subwalk of W;
s is_Walk_from W .first() ,W .last() by GLIB_001:def 32;
then ( len s <= len W & len W <= len s ) by A1, Def2, GLIB_001:163;
hence contradiction by A2, Th35, XXREAL_0:1; :: thesis: verum