let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)

for i being Nat st p in LSeg (f,i) holds

p in L~ f

let p be Point of (TOP-REAL 2); :: thesis: for i being Nat st p in LSeg (f,i) holds

p in L~ f

let i be Nat; :: thesis: ( p in LSeg (f,i) implies p in L~ f )

LSeg (f,i) c= L~ f by TOPREAL3:19;

hence ( p in LSeg (f,i) implies p in L~ f ) ; :: thesis: verum

for i being Nat st p in LSeg (f,i) holds

p in L~ f

let p be Point of (TOP-REAL 2); :: thesis: for i being Nat st p in LSeg (f,i) holds

p in L~ f

let i be Nat; :: thesis: ( p in LSeg (f,i) implies p in L~ f )

LSeg (f,i) c= L~ f by TOPREAL3:19;

hence ( p in LSeg (f,i) implies p in L~ f ) ; :: thesis: verum