let G be _Graph; :: thesis: for v being Vertex of G
for W being Walk of G st W is_Walk_from v,v holds
( W is minlength iff W = G .walkOf v )
let v be Vertex of G; :: thesis: for W being Walk of G st W is_Walk_from v,v holds
( W is minlength iff W = G .walkOf v )
let W be Walk of G; :: thesis: ( W is_Walk_from v,v implies ( W is minlength iff W = G .walkOf v ) )
assume A1: W is_Walk_from v,v ; :: thesis: ( W is minlength iff W = G .walkOf v )

hereby :: thesis: ( W = G .walkOf v implies W is minlength )

assume A2: W is minlength ; :: thesis: W = G .walkOf v
G .walkOf v is_Walk_from v,v by GLIB_001:13;
then G .walkOf v is_Walk_from W .first() ,v by A1, GLIB_001:def 23;
then G .walkOf v is_Walk_from W .first() ,W .last() by A1, GLIB_001:def 23;
then len (G .walkOf v) >= len W by A2, CHORD:def 2;
then A3: 1 >= len W by GLIB_001:13;
1 <= len W by CHORD:2;
then W is trivial by A3, XXREAL_0:1, GLIB_001:126;
then consider v0 being Vertex of G such that
A4: W = G .walkOf v0 by GLIB_001:128;
W .first() = v0 by A4;
hence W = G .walkOf v by A1, A4, GLIB_001:def 23; :: thesis: verum

end;

assume A5: W = G .walkOf v ; :: thesis: W is minlength

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

let W9 be Walk of G; :: thesis: ( W9 is_Walk_from W .first() ,W .last() implies len W9 >= len W )
assume W9 is_Walk_from W .first() ,W .last() ; :: thesis: len W9 >= len W
len W9 >= 1 by CHORD:2;
hence len W9 >= len W by A5, GLIB_001:13; :: thesis: verum

end;

hence W is minlength by CHORD:def 2; :: thesis: verum