theorem :: GLIB_001:154

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