let G1 be _Graph; :: thesis: for E being set
for G2 being reverseEdgeDirections of G1,E
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is minlength holds
W2 is minlength
let E be set ; :: thesis: for G2 being reverseEdgeDirections of G1,E
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is minlength holds
W2 is minlength
let G2 be reverseEdgeDirections of G1,E; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is minlength holds
W2 is minlength
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 = W2 & W1 is minlength holds
W2 is minlength
let W2 be Walk of G2; :: thesis: ( W1 = W2 & W1 is minlength implies W2 is minlength )
assume A1: ( W1 = W2 & W1 is minlength ) ; :: thesis: W2 is minlength

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

let W4 be Walk of G2; :: thesis: ( W4 is_Walk_from W2 .first() ,W2 .last() implies len W4 >= len W2 )
reconsider W3 = W4 as Walk of G1 by GLIB_007:15;
assume W4 is_Walk_from W2 .first() ,W2 .last() ; :: thesis: len W4 >= len W2
then W3 is_Walk_from W2 .first() ,W2 .last() by GLIB_001:19;
then W3 is_Walk_from W1 .first() ,W2 .last() by A1;
then W3 is_Walk_from W1 .first() ,W1 .last() by A1;
hence len W4 >= len W2 by A1, CHORD:def 2; :: thesis: verum

end;

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