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:28;
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 4;
then not (Index p,f) + 1 in dom f by A2, A3, SPRECT_2:11;
then ( (Index p,f) + 1 < 1 or (Index p,f) + 1 > len f ) by FINSEQ_3:27;
then Index p,f >= len f by NAT_1:11, NAT_1:13;
hence contradiction by A1, JORDAN3:41; :: thesis: verum