theorem :: CHORD:93

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
( P .cut (m,n) is chordless & P .cut (m,n) is open )