theorem :: CHORD:43

for G being _Graph st G is connected holds
for A, B being non empty Subset of (the_Vertices_of G) st A misses B holds
ex P being Path of G st
( P is minlength & P is trivial & P .first() in A & P .last() in B & ( for n being odd Nat st 1 < n & n < len P holds
( not P . n in A & not P . n in B ) ) )