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:26;
then consider S being non empty Subset of NAT such that
A2: Index p,f = min S and
A3: S = { i where i is Element of NAT : p in LSeg f,i } by A1, Def2;
i0 in S by A1, A3;
hence Index p,f <= i0 by A2, XXREAL_2:def 7; :: thesis: verum