theorem :: SPPOL_2:16

for f being FinSequence of (TOP-REAL 2)
for i being Nat st 1 <= i & i + 1 <= len f holds
LSeg ((f /. i),(f /. (i + 1))) c= L~ f