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