theorem Th35: :: SPPOL_1:35

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & f /. (i + 1) in LSeg (p,q) & LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & not f /. (i + 1) = p holds
f /. (i + 1) = q