let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)
for i being Element of NAT st 1 <= i & i + 1 <= len f & p in LSeg (f /. i),(f /. (i + 1)) holds
p in L~ f
let p be Point of (TOP-REAL 2); :: thesis: for i being Element of NAT st 1 <= i & i + 1 <= len f & p in LSeg (f /. i),(f /. (i + 1)) holds
p in L~ f
let i be Element of NAT ; :: thesis: ( 1 <= i & i + 1 <= len f & p in LSeg (f /. i),(f /. (i + 1)) implies p in L~ f )
assume that
A1: 1 <= i and
A2: i + 1 <= len f and
A3: p in LSeg (f /. i),(f /. (i + 1)) ; :: thesis: p in L~ f
set X = { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ;
A4: LSeg f,i in { (LSeg f,j) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A1, A2;
LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A1, A2, TOPREAL1:def 5;
hence p in L~ f by A3, A4, TARSKI:def 4; :: thesis: verum