theorem Th23: :: JORDAN9:23

for k being Nat
for G being Go-board
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st 2 <= len G & 2 <= width G & f is_sequence_on G & 1 <= k & k + 1 <= len f & p in Values G & p in LSeg (f,k) & not p = f /. k holds
p = f /. (k + 1)