theorem Th65: :: GLIB_001:67

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