theorem Th91: :: CHORD:92

for G being _Graph
for P being Path of G st P is open & P is chordless holds
for m, n being odd Nat st m < n & n <= len P holds
( ex e being object st e Joins P . m,P . n,G iff m + 2 = n )