let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st G1 == G2 & W1 = W2 & W1 is minlength holds
W2 is minlength
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st G1 == G2 & W1 = W2 & W1 is minlength holds
W2 is minlength
let W2 be Walk of G2; :: thesis: ( G1 == G2 & W1 = W2 & W1 is minlength implies W2 is minlength )
assume A1: ( G1 == G2 & 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 )
assume A2: W4 is_Walk_from W2 .first() ,W2 .last() ; :: thesis: len W4 >= len W2
reconsider W3 = W4 as Walk of G1 by A1, GLIB_001:179;
W3 is_Walk_from W2 .first() ,W2 .last() by A2, GLIB_001:19;
then W3 is_Walk_from W1 .first() ,W2 .last() by A1, GLIB_001:16;
then W3 is_Walk_from W1 .first() ,W1 .last() by A1, GLIB_001:16;
hence len W4 >= len W2 by A1, CHORD:def 2; :: thesis: verum

end;

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