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 b1 >= len W )
assume W2 is_Walk_from W .first() ,W .last() ; :: thesis: len b1 >= len W
per cases ( not W2 is V5() or not W2 is V5() ) ;
end;
end;
hence W is minlength by CHORD:def 2; :: thesis: verum