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