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 Th42;
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, Th40;
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 9; :: thesis: verum