for G being _Graph
for W being Walk of G holds len W = (2 * (W .length())) + 1 by Def15;