let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)
for i being Element of NAT st p in LSeg (f,i) holds
Index (p,f) <= i
let p be Point of (TOP-REAL 2); :: thesis: for i being Element of NAT st p in LSeg (f,i) holds
Index (p,f) <= i
let i0 be Element of NAT ; :: thesis: ( p in LSeg (f,i0) implies Index (p,f) <= i0 )
assume A1: p in LSeg (f,i0) ; :: thesis: Index (p,f) <= i0
LSeg (f,i0) c= L~ f by TOPREAL3:19;
then consider S being non empty Subset of NAT such that
A2: Index (p,f) = min S and
A3: S = { i where i is Nat : p in LSeg (f,i) } by A1, Def1;
i0 in S by A1, A3;
hence Index (p,f) <= i0 by A2, XXREAL_2:def 7; :: thesis: verum