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