let f be FinSequence of (); :: thesis: for p being Point of ()
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 (); :: 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 ;
then p in LSeg (f,(Index (p,f))) by Th9;
then p in (LSeg (f,(Index (p,f)))) /\ (LSeg (f,i1)) by ;
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 ;
then Index (p,f) < i1 by ;
then (Index (p,f)) + 1 <= i1 by NAT_1:13;
then (Index (p,f)) + 1 < i1 by ;
hence contradiction by A1, A3, TOPREAL1:def 7; :: thesis: verum