theorem
for
f being
FinSequence of
(TOP-REAL 2) for
Q being
Subset of
(TOP-REAL 2) for
q being
Point of
(TOP-REAL 2) for
i,
j being
Nat st
L~ f meets Q &
f is
being_S-Seq &
Q is
closed &
First_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
in LSeg (
f,
i) & 1
<= i &
i + 1
<= len f &
q in LSeg (
f,
j) & 1
<= j &
j + 1
<= len f &
q in Q &
First_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
<> q holds
(
i <= j & (
i = j implies
LE First_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q),
q,
f /. i,
f /. (i + 1) ) )