let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
L_Cut (f,p) <> {}
let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies L_Cut (f,p) <> {} )
assume that
A1: p in L~ f and
A2: L_Cut (f,p) = {} ; :: thesis: contradiction
len f <> 0 by A1, TOPREAL1:22;
then f <> {} ;
then A3: len f in dom f by FINSEQ_5:6;
A4: ( p <> f . ((Index (p,f)) + 1) or p = f . ((Index (p,f)) + 1) ) ;
not <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) is empty ;
then L_Cut (f,p) = mid (f,((Index (p,f)) + 1),(len f)) by A2, A4, JORDAN3:def 3;
then not (Index (p,f)) + 1 in dom f by A2, A3, SPRECT_2:7;
then ( (Index (p,f)) + 1 < 1 or (Index (p,f)) + 1 > len f ) by FINSEQ_3:25;
then Index (p,f) >= len f by NAT_1:11, NAT_1:13;
hence contradiction by A1, JORDAN3:8; :: thesis: verum