theorem Th22: :: CHORD:22

for G being _Graph
for a, b being set st a <> b holds
for W being Walk of G st W .vertices() = {a,b} holds
ex e being set st e Joins a,b,G