for G being _finite _Graph
for W being Path of G holds len (W .vertexSeq()) <= (G .order()) + 1