theorem :: HELLY:11

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