theorem :: HELLY:14

for G being _Graph
for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds
W1 .edges() c= W2 .edges()