theorem :: SPPOL_1:21

for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2) st f is one-to-one & 1 <= i & i + 1 <= len f & LSeg (f,i) is vertical holds
not LSeg (f,i) is horizontal by Lm1, Th20;