let G be _Graph; :: thesis: for W being Walk of G st ( for P being Path of G st P is_Walk_from W .first() ,W .last() holds
len P >= len W ) holds
W is minlength
let W be Walk of G; :: thesis: ( ( for P being Path of G st P is_Walk_from W .first() ,W .last() holds
len P >= len W ) implies W is minlength )
assume A1: for P2 being Path of G st P2 is_Walk_from W .first() ,W .last() holds
len P2 >= len W ; :: thesis: W is minlength

now :: thesis: for V being Walk of G st V is_Walk_from W .first() ,W .last() holds
len V >= len W

let V be Walk of G; :: thesis: ( V is_Walk_from W .first() ,W .last() implies len V >= len W )
assume A2: V is_Walk_from W .first() ,W .last() ; :: thesis: len V >= len W
set P3 = the Path-like Subwalk of V;
V .last() = W .last() by A2;
then A3: the Path-like Subwalk of V .last() = W .last() by GLIB_001:161;
V .first() = W .first() by A2;
then the Path-like Subwalk of V .first() = W .first() by GLIB_001:161;
then the Path-like Subwalk of V is_Walk_from W .first() ,W .last() by A3;
then A4: len W <= len the Path-like Subwalk of V by A1;
len the Path-like Subwalk of V <= len V by GLIB_001:162;
hence len V >= len W by A4, XXREAL_0:2; :: thesis: verum

end;

hence W is minlength ; :: thesis: verum