theorem Th71: :: CHORD:72

for G being _Graph
for a, b being Vertex of G st a <> b & not a,b are_adjacent holds
for S being VertexSeparator of a,b
for W being Walk of G st W is_Walk_from a,b holds
ex k being odd Nat st
( 1 < k & k < len W & W . k in S )