theorem Th13: :: HELLY:13

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