theorem Th32: :: SPPOL_1:32

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 & LSeg (f,i) is vertical holds
LSeg (f,(i + 1)) is horizontal