let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)

for i being 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 Nat st 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) holds

p in L~ f

let i be 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 Nat : ( 1 <= j & j + 1 <= len f ) } ;

A4: LSeg (f,i) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A1, A2;

LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A1, A2, TOPREAL1:def 3;

hence p in L~ f by A3, A4, TARSKI:def 4; :: thesis: verum

for i being 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 Nat st 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) holds

p in L~ f

let i be 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 Nat : ( 1 <= j & j + 1 <= len f ) } ;

A4: LSeg (f,i) in { (LSeg (f,j)) where j is Nat : ( 1 <= j & j + 1 <= len f ) } by A1, A2;

LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A1, A2, TOPREAL1:def 3;

hence p in L~ f by A3, A4, TARSKI:def 4; :: thesis: verum