let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)

for i1 being Element of NAT st f is s.n.c. & p in LSeg (f,i1) & not i1 = Index (p,f) holds

i1 = (Index (p,f)) + 1

let p be Point of (TOP-REAL 2); :: thesis: for i1 being Element of NAT st f is s.n.c. & p in LSeg (f,i1) & not i1 = Index (p,f) holds

i1 = (Index (p,f)) + 1

let i1 be Element of NAT ; :: thesis: ( f is s.n.c. & p in LSeg (f,i1) & not i1 = Index (p,f) implies i1 = (Index (p,f)) + 1 )

assume that

A1: f is s.n.c. and

A2: p in LSeg (f,i1) ; :: thesis: ( i1 = Index (p,f) or i1 = (Index (p,f)) + 1 )

p in L~ f by A2, SPPOL_2:17;

then p in LSeg (f,(Index (p,f))) by Th9;

then p in (LSeg (f,(Index (p,f)))) /\ (LSeg (f,i1)) by A2, XBOOLE_0:def 4;

then A3: LSeg (f,(Index (p,f))) meets LSeg (f,i1) by XBOOLE_0:4;

assume A4: ( not i1 = Index (p,f) & not i1 = (Index (p,f)) + 1 ) ; :: thesis: contradiction

Index (p,f) <= i1 by A2, Th7;

then Index (p,f) < i1 by A4, XXREAL_0:1;

then (Index (p,f)) + 1 <= i1 by NAT_1:13;

then (Index (p,f)) + 1 < i1 by A4, XXREAL_0:1;

hence contradiction by A1, A3, TOPREAL1:def 7; :: thesis: verum

for i1 being Element of NAT st f is s.n.c. & p in LSeg (f,i1) & not i1 = Index (p,f) holds

i1 = (Index (p,f)) + 1

let p be Point of (TOP-REAL 2); :: thesis: for i1 being Element of NAT st f is s.n.c. & p in LSeg (f,i1) & not i1 = Index (p,f) holds

i1 = (Index (p,f)) + 1

let i1 be Element of NAT ; :: thesis: ( f is s.n.c. & p in LSeg (f,i1) & not i1 = Index (p,f) implies i1 = (Index (p,f)) + 1 )

assume that

A1: f is s.n.c. and

A2: p in LSeg (f,i1) ; :: thesis: ( i1 = Index (p,f) or i1 = (Index (p,f)) + 1 )

p in L~ f by A2, SPPOL_2:17;

then p in LSeg (f,(Index (p,f))) by Th9;

then p in (LSeg (f,(Index (p,f)))) /\ (LSeg (f,i1)) by A2, XBOOLE_0:def 4;

then A3: LSeg (f,(Index (p,f))) meets LSeg (f,i1) by XBOOLE_0:4;

assume A4: ( not i1 = Index (p,f) & not i1 = (Index (p,f)) + 1 ) ; :: thesis: contradiction

Index (p,f) <= i1 by A2, Th7;

then Index (p,f) < i1 by A4, XXREAL_0:1;

then (Index (p,f)) + 1 <= i1 by NAT_1:13;

then (Index (p,f)) + 1 < i1 by A4, XXREAL_0:1;

hence contradiction by A1, A3, TOPREAL1:def 7; :: thesis: verum