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