theorem Th20:
for
f being
FinSequence of
(TOP-REAL 2) for
Q being
Subset of
(TOP-REAL 2) for
i being
Nat st
L~ f meets Q &
Q is
closed &
f is
being_S-Seq & 1
<= i &
i + 1
<= len f &
Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
in LSeg (
f,
i) holds
Last_Point (
(L~ f),
(f /. 1),
(f /. (len f)),
Q)
= Last_Point (
(LSeg (f,i)),
(f /. i),
(f /. (i + 1)),
Q)