let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds

ex i being Nat st

( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) )

let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies ex i being Nat st

( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) ) )

assume p in L~ f ; :: thesis: ex i being Nat st

( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) )

then consider i being Nat such that

A1: 1 <= i and

A2: i + 1 <= len f and

A3: p in LSeg (f,i) by Th13;

take i ; :: thesis: ( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) )

thus ( 1 <= i & i + 1 <= len f ) by A1, A2; :: thesis: p in LSeg ((f /. i),(f /. (i + 1)))

thus p in LSeg ((f /. i),(f /. (i + 1))) by A1, A2, A3, TOPREAL1:def 3; :: thesis: verum

ex i being Nat st

( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) )

let p be Point of (TOP-REAL 2); :: thesis: ( p in L~ f implies ex i being Nat st

( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) ) )

assume p in L~ f ; :: thesis: ex i being Nat st

( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) )

then consider i being Nat such that

A1: 1 <= i and

A2: i + 1 <= len f and

A3: p in LSeg (f,i) by Th13;

take i ; :: thesis: ( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) )

thus ( 1 <= i & i + 1 <= len f ) by A1, A2; :: thesis: p in LSeg ((f /. i),(f /. (i + 1)))

thus p in LSeg ((f /. i),(f /. (i + 1))) by A1, A2, A3, TOPREAL1:def 3; :: thesis: verum