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 A1: ( f = <*p,p1,q*> & i <> 0 & j > i + 1 ) ; :: thesis: LSeg f,j = {}
then i > 0 ;
then i >= 0 + 1 by NAT_1:13;
then ( 1 + i >= 1 + 1 & j > 1 + i ) by A1, XREAL_1:9;
then j > 2 by XXREAL_0:2;
then j >= 2 + 1 by NAT_1:13;
then ( j + 1 > 3 & len f = 3 ) by A1, FINSEQ_1:62, NAT_1:13;
hence LSeg f,j = {} by TOPREAL1:def 5; :: thesis: verum