let f be FinSequence of ; :: thesis: for p being Point of
for i being Element of NAT st p in LSeg f,i holds
p in L~ f
let p be Point of ; :: 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