for G1 being _Graph
for G2 being removeLoops of G1
for W1 being minlength Walk of G1 holds W1 is Walk of G2