let G1 be _Graph; :: thesis: for G2 being removeLoops of G1
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( W1 is minlength iff W2 is minlength )
let G2 be removeLoops of G1; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( W1 is minlength iff W2 is minlength )
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 holds
( W1 is minlength iff W2 is minlength )
let W2 be Walk of G2; :: thesis: ( W1 = W2 implies ( W1 is minlength iff W2 is minlength ) )
assume A1: W1 = W2 ; :: thesis: ( W1 is minlength iff W2 is minlength )
hence ( W1 is minlength implies W2 is minlength ) by Th47; :: thesis: ( W2 is minlength implies W1 is minlength )
assume A2: W2 is minlength ; :: thesis: W1 is minlength

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

let W be Walk of G1; :: thesis: ( W is_Walk_from W1 .first() ,W1 .last() implies len b₁ >= len W1 )
set P = the Path of W;
assume W is_Walk_from W1 .first() ,W1 .last() ; :: thesis: len b₁ >= len W1
then A3: the Path of W is_Walk_from W1 .first() ,W1 .last() by GLIB_001:160;

per cases ( the Path of W .edges() misses G1 .loops() or ex v, e being object st
( e Joins v,v,G1 & the Path of W = G1 .walkOf (v,e,v) ) ) by GLIB_009:57;

suppose the Path of W .edges() misses G1 .loops() ; :: thesis: len b₁ >= len W1

then reconsider W9 = the Path of W as Walk of G2 by Th38;
W9 is_Walk_from W1 .first() ,W1 .last() by A3, GLIB_001:19;
then W9 is_Walk_from W2 .first() ,W1 .last() by A1;
then W9 is_Walk_from W2 .first() ,W2 .last() by A1;
then A4: len the Path of W >= len W1 by A1, A2, CHORD:def 2;
len W >= len the Path of W by GLIB_001:162;
hence len W >= len W1 by A4, XXREAL_0:2; :: thesis: verum

end;

suppose ex v, e being object st
( e Joins v,v,G1 & the Path of W = G1 .walkOf (v,e,v) ) ; :: thesis: len b₁ >= len W1

then consider v, e being object such that
A5: ( e Joins v,v,G1 & the Path of W = G1 .walkOf (v,e,v) ) ;
( the Path of W .first() = v & the Path of W .last() = v ) by A5, GLIB_001:15;
then ( W1 .first() = v & W1 .last() = v ) by A3, GLIB_001:def 23;
then A6: ( W2 .first() = v & W2 .last() = v ) by A1;
then reconsider v = v as Vertex of G2 ;
W2 is_Walk_from v,v by A6, GLIB_001:def 23;
then W2 = G2 .walkOf v by A2, Th48;
then A7: ( len the Path of W = 3 & len W2 = 1 ) by A5, GLIB_001:13, GLIB_001:14;
len W >= len the Path of W by GLIB_001:162;
hence len W >= len W1 by A1, A7, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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