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

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