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