let G1 be _Graph; :: thesis: for G2 being removeLoops of G1
for W1 being minlength Walk of G1 holds W1 is Walk of G2
let G2 be removeLoops of G1; :: thesis: for W1 being minlength Walk of G1 holds W1 is Walk of G2
let W1 be minlength Walk of G1; :: thesis: W1 is Walk of G2
reconsider P = W1 as Path of G1 by CHORD:36;

now :: thesis: not P .edges() meets G1 .loops()

assume P .edges() meets G1 .loops() ; :: thesis: contradiction
then consider v, e being object such that
A1: ( e Joins v,v,G1 & P = G1 .walkOf (v,e,v) ) by GLIB_009:57;
reconsider v = v as Vertex of G1 by A1, GLIB_000:13;
A2: ( P .first() = v & P .last() = v & len P = 3 ) by A1, GLIB_001:14, GLIB_001:15;
len (G1 .walkOf v) = 1 by GLIB_001:13;
hence contradiction by A2, GLIB_001:13, CHORD:def 2; :: thesis: verum

end;

hence W1 is Walk of G2 by Th38; :: thesis: verum