theorem Th29: :: SPPOL_1:29

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) holds
( p1 `2 = p2 `2 & p3 `2 <> p2 `2 )