theorem Th29:
for
f being
FinSequence of
(TOP-REAL 2) for
q1,
q2 being
Point of
(TOP-REAL 2) for
i being
Nat st
q1 in LSeg (
f,
i) &
q2 in LSeg (
f,
i) &
f is
being_S-Seq & 1
<= i &
i + 1
<= len f &
LE q1,
q2,
L~ f,
f /. 1,
f /. (len f) holds
LE q1,
q2,
LSeg (
f,
i),
f /. i,
f /. (i + 1)