theorem Th37: :: SPPOL_1:37

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2)
for u being Point of (Euclid 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg (p,q) & f /. (i + 1) <> q & not p in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) holds
for s being Real st s > 0 holds
ex p3 being Point of (TOP-REAL 2) st
( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) )