theorem :: HELLY:11

for G being _Graph
for W being Walk of G
for m, n being Nat st W .cut (m,n) is V5() holds
not W is V5()