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:70;
then A3: len (R_Cut f,p) >= 2 by TOPREAL1:def 10;
(R_Cut f,p) . (len (R_Cut f,p)) = p by A1, JORDAN3:59;
hence p in L~ (R_Cut f,p) by A3, JORDAN3:34; :: thesis: verum