theorem :: JORDAN5B:30

for f being FinSequence of (TOP-REAL 2)
for i being Nat st f is unfolded & f is s.n.c. & f is one-to-one & len f >= 2 & f /. 1 in LSeg (f,i) holds
i = 1