let f be FinSequence of (TOP-REAL 2); 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); for i being Element of NAT st p in LSeg (f,i) holds
Index (p,f) <= i
let i0 be Element of NAT ; ( p in LSeg (f,i0) implies Index (p,f) <= i0 )
assume A1:
p in LSeg (f,i0)
; 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; verum