theorem :: JORDAN5C:21

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