let G1 be _Graph; :: thesis: for G2 being Subgraph of G1
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 Subgraph of G1; :: 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 W9 being Walk of G2 holds
( not W9 is_Walk_from W2 .first() ,W2 .last() or not len W9 < len W2 )

given W9 being Walk of G2 such that A2: ( W9 is_Walk_from W2 .first() ,W2 .last() & len W9 < len W2 ) ; :: thesis: contradiction
reconsider W8 = W9 as Walk of G1 by GLIB_001:167;
W8 is_Walk_from W2 .first() ,W2 .last() by A2, GLIB_001:19;
then W8 is_Walk_from W1 .first() ,W2 .last() by A1;
then W8 is_Walk_from W1 .first() ,W1 .last() by A1;
hence contradiction by A1, A2, CHORD:def 2; :: thesis: verum

end;

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