theorem :: SPPOL_1:34

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 & not ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) holds
( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical ) by Th32, Th19, Th33;