theorem :: GLIB_009:28

for G being _Graph
for W being Walk of G holds len (W .vertexSeq()) = (W .length()) + 1