theorem
for
f being
FinSequence of
(TOP-REAL 2) for
p,
q being
Point of
(TOP-REAL 2) st
p in L~ f &
q in L~ f & (
Index (
p,
f)
< Index (
q,
f) or (
Index (
p,
f)
= Index (
q,
f) &
LE p,
q,
f /. (Index (p,f)),
f /. ((Index (p,f)) + 1) ) ) &
p <> q holds
L~ (B_Cut (f,p,q)) c= L~ f by Lm3;