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

for i, j being Nat st f = <*p,p1,q*> & i <> 0 & j > i + 1 holds

LSeg (f,j) = {}

let f be FinSequence of (TOP-REAL 2); :: thesis: for i, j being Nat st f = <*p,p1,q*> & i <> 0 & j > i + 1 holds

LSeg (f,j) = {}

let i, j be Nat; :: thesis: ( f = <*p,p1,q*> & i <> 0 & j > i + 1 implies LSeg (f,j) = {} )

assume that

A1: f = <*p,p1,q*> and

A2: i <> 0 and

A3: j > i + 1 ; :: thesis: LSeg (f,j) = {}

i >= 0 + 1 by A2, NAT_1:13;

then 1 + i >= 1 + 1 by XREAL_1:7;

then j > 2 by A3, XXREAL_0:2;

then j >= 2 + 1 by NAT_1:13;

then A4: j + 1 > 3 by NAT_1:13;

len f = 3 by A1, FINSEQ_1:45;

hence LSeg (f,j) = {} by A4, TOPREAL1:def 3; :: thesis: verum

for i, j being Nat st f = <*p,p1,q*> & i <> 0 & j > i + 1 holds

LSeg (f,j) = {}

let f be FinSequence of (TOP-REAL 2); :: thesis: for i, j being Nat st f = <*p,p1,q*> & i <> 0 & j > i + 1 holds

LSeg (f,j) = {}

let i, j be Nat; :: thesis: ( f = <*p,p1,q*> & i <> 0 & j > i + 1 implies LSeg (f,j) = {} )

assume that

A1: f = <*p,p1,q*> and

A2: i <> 0 and

A3: j > i + 1 ; :: thesis: LSeg (f,j) = {}

i >= 0 + 1 by A2, NAT_1:13;

then 1 + i >= 1 + 1 by XREAL_1:7;

then j > 2 by A3, XXREAL_0:2;

then j >= 2 + 1 by NAT_1:13;

then A4: j + 1 > 3 by NAT_1:13;

len f = 3 by A1, FINSEQ_1:45;

hence LSeg (f,j) = {} by A4, TOPREAL1:def 3; :: thesis: verum