theorem Th20: :: SPPOL_1:20

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 holds
not LSeg (f,i) is trivial