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