let p, p1, q be Point of (TOP-REAL 2); 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); for i, j being Nat st f = <*p,p1,q*> & i <> 0 & j > i + 1 holds
LSeg (f,j) = {}
let i, j be Nat; ( 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
; 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; verum