theorem Th17: :: HELLY:17

for G being _Graph
for W1, W2 being Trail of G st W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() holds
W1 .append W2 is Trail-like