theorem Th10: :: HELLY:10

for G being _Graph
for W being Walk of G
for m, n being Nat holds len (W .cut (m,n)) <= len W