theorem Th25: :: CHORD:25

for G being _Graph
for P being Path of G
for m, n being odd Nat st m <= len P & n <= len P & P . m = P . n & not m = n & not ( m = 1 & n = len P ) holds
( m = len P & n = 1 )