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 . (len f) holds
p in L~ (L_Cut f,p)
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f & f is being_S-Seq & p <> f . (len f) implies p in L~ (L_Cut f,p) )
assume that
A1: p in L~ f and
A2: f is being_S-Seq ; :: thesis: ( not p <> f . (len f) or p in L~ (L_Cut f,p) )
assume p <> f . (len f) ; :: thesis: p in L~ (L_Cut f,p)
then L_Cut f,p is being_S-Seq by A1, A2, JORDAN3:69;
then A3: len (L_Cut f,p) >= 2 by TOPREAL1:def 10;
(L_Cut f,p) . 1 = p by A1, JORDAN3:58;
hence p in L~ (L_Cut f,p) by A3, JORDAN3:34; :: thesis: verum