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

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