theorem :: GLIB_001:74

for G being _Graph
for W being Walk of G
for n being Element of NAT holds (W .cut (1,n)) .vertexSeq() c= W .vertexSeq()