theorem Th36: :: SPPOL_1:36

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