let f be FinSequence of (TOP-REAL 2); for p being Point of (TOP-REAL 2) st p in L~ f & f is being_S-Seq & p <> f . 1 holds
p in L~ (R_Cut (f,p))
let p be Point of (TOP-REAL 2); ( p in L~ f & f is being_S-Seq & p <> f . 1 implies p in L~ (R_Cut (f,p)) )
assume that
A1:
p in L~ f
and
A2:
f is being_S-Seq
; ( not p <> f . 1 or p in L~ (R_Cut (f,p)) )
assume
p <> f . 1
; p in L~ (R_Cut (f,p))
then
R_Cut (f,p) is being_S-Seq
by A1, A2, JORDAN3:35;
then A3:
len (R_Cut (f,p)) >= 2
by TOPREAL1:def 8;
(R_Cut (f,p)) . (len (R_Cut (f,p))) = p
by A1, JORDAN3:24;
hence
p in L~ (R_Cut (f,p))
by A3, JORDAN3:1; verum