theorem Th12: :: HELLY:12

for G being _Graph
for W being Walk of G
for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds
ex j being odd Nat st
( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )