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

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

hence
W is minlength
; :: thesis: verumlen 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;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