theorem :: GLIB_001:112

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