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
p in L~ f
let p be Point of (TOP-REAL 2); :: thesis: for i being Element of NAT st p in LSeg f,i holds
p in L~ f
let i be Element of NAT ; :: thesis: ( p in LSeg f,i implies p in L~ f )
LSeg f,i c= L~ f by TOPREAL3:26;
hence ( p in LSeg f,i implies p in L~ f ) ; :: thesis: verum