set W2 = W .reverse() ;
now :: thesis: for W3 being Walk of G st W3 is_Walk_from (W .reverse()) .first() ,(W .reverse()) .last() holds
len W3 >= len (W .reverse())
let W3 be Walk of G; :: thesis: ( W3 is_Walk_from (W .reverse()) .first() ,(W .reverse()) .last() implies len W3 >= len (W .reverse()) )
assume W3 is_Walk_from (W .reverse()) .first() ,(W .reverse()) .last() ; :: thesis: len W3 >= len (W .reverse())
then W3 .reverse() is_Walk_from (W .reverse()) .last() ,(W .reverse()) .first() by GLIB_001:23;
then W3 .reverse() is_Walk_from W .first() ,(W .reverse()) .first() by GLIB_001:22;
then W3 .reverse() is_Walk_from W .first() ,W .last() by GLIB_001:22;
then len (W3 .reverse()) >= len W by CHORD:def 2;
then len W3 >= len W by GLIB_001:21;
hence len W3 >= len (W .reverse()) by GLIB_001:21; :: thesis: verum
end;
hence W .reverse() is minlength by CHORD:def 2; :: thesis: verum