let f be FinSequence of (TOP-REAL 2); :: thesis: 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); :: thesis: ( 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 ; :: thesis: ( not p <> f . 1 or p in L~ (R_Cut (f,p)) )
assume p <> f . 1 ; :: thesis: 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; :: thesis: verum