theorem Th16: :: HELLY:16

for G being _Graph
for W1, W2 being Walk of G st W1 is trivial & W1 .last() = W2 .first() holds
W1 .append W2 = W2