let W be Walk of G; :: thesis: ( W is V5() implies W is minlength )
assume W is V5() ; :: thesis: W is minlength
then A1: len W = 1 by GLIB_001:126;

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

let W2 be Walk of G; :: thesis: ( W2 is_Walk_from W .first() ,W .last() implies len b₁ >= len W )
assume W2 is_Walk_from W .first() ,W .last() ; :: thesis: len b₁ >= len W

per cases ( not W2 is V5() or not W2 is V5() ) ;

suppose W2 is V5() ; :: thesis: len b₁ >= len W

hence len W2 >= len W by A1, GLIB_001:126; :: thesis: verum

end;

suppose W2 is V5() ; :: thesis: len b₁ >= len W

then ( len W2 >= 3 & 3 >= 1 ) by GLIB_001:125;
hence len W2 >= len W by A1, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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