theorem Th14: :: SPPOL_2:14

for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
ex i being Nat st
( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) )