let j be Nat; :: thesis:
let f be S-Sequence_in_R2; :: thesis:
let p, q be Point of (TOP-REAL 2); :: thesis:
assume that
A1: 1 <= j and
A2: j < len f and
A3: p in LSeg (f,j) and
A4: q in LSeg ((f /. j),p) ; :: thesis:
A5: j + 1 <= len f by A2, NAT_1:13;
then A6: LSeg (f,j) = LSeg ((f /. j),(f /. (j + 1))) by A1, TOPREAL1:def 3;
A7: f /. j in LSeg (f,j) by A1, A5, TOPREAL1:21;
then A8: LSeg ((f /. j),p) c= LSeg (f,j) by A3, A6, TOPREAL1:6;
then A9: q in LSeg (f,j) by A4;
A10: LSeg (f,j) c= L~ f by TOPREAL3:19;

suppose p = q ; :: thesis:

hence LE q,p, L~ f,f /. 1,f /. (len f) by A3, A10, JORDAN5C:9; :: thesis:

end;

suppose A11: q <> p ; :: thesis:

for i, j being Nat st q in LSeg (f,i) & p in LSeg (f,j) & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q,p,f /. i,f /. (i + 1) ) )

1 <= j + 1 by NAT_1:11;
then A12: j + 1 in dom f by A5, FINSEQ_3:25;
let i1, i2 be Nat; :: thesis:
assume that
A13: q in LSeg (f,i1) and
A14: p in LSeg (f,i2) and
1 <= i1 and
A15: i1 + 1 <= len f and
A16: 1 <= i2 and
i2 + 1 <= len f ; :: thesis:
A17: p in (LSeg (f,i2)) /\ (LSeg (f,j)) by A3, A14, XBOOLE_0:def 4;
then A18: LSeg (f,i2) meets LSeg (f,j) ;
then A19: j + 1 >= i2 by TOPREAL1:def 7;
A20: q in (LSeg (f,i1)) /\ (LSeg (f,j)) by A4, A8, A13, XBOOLE_0:def 4;
then A21: LSeg (f,i1) meets LSeg (f,j) ;
then A22: i1 + 1 >= j by TOPREAL1:def 7;

A23: now :: thesis:

assume A24: i2 + 1 = j ; :: thesis:
i2 + (1 + 1) = (i2 + 1) + 1 ;
then i2 + 2 <= len f by A2, A24, NAT_1:13;
then p in {(f /. j)} by A16, A17, A24, TOPREAL1:def 6;
then p = f /. j by TARSKI:def 1;
then q in {p} by A4, RLTOPSP1:70;
hence contradiction by A11, TARSKI:def 1; :: thesis:

end;

A25: now :: thesis:

assume that
A26: i2 + 1 > j and
A27: j + 1 > i2 ; :: thesis:
A28: j <= i2 by A26, NAT_1:13;
i2 <= j by A27, NAT_1:13;
hence i2 = j by A28, XXREAL_0:1; :: thesis:

end;

i2 + 1 >= j by A18, TOPREAL1:def 7;
then ( i2 + 1 = j or i2 = j or j + 1 = i2 ) by A25, A19, XXREAL_0:1;
then A29: i2 >= j by A23, NAT_1:11;

A30: now :: thesis:

assume that
A31: i1 + 1 > j and
A32: j + 1 > i1 ; :: thesis:
A33: j <= i1 by A31, NAT_1:13;
i1 <= j by A32, NAT_1:13;
hence i1 = j by A33, XXREAL_0:1; :: thesis:

end;

A34: j in dom f by A1, A2, FINSEQ_3:25;

A35: now :: thesis:

assume f /. (j + 1) = f /. j ; :: thesis:
then j = j + 1 by A12, A34, PARTFUN2:10;
hence contradiction ; :: thesis:

end;

A36: now :: thesis:

A37: j + (1 + 1) = (j + 1) + 1 ;
assume i1 = j + 1 ; :: thesis:
then q in {(f /. (j + 1))} by A1, A15, A20, A37, TOPREAL1:def 6;
then q = f /. (j + 1) by TARSKI:def 1;
hence contradiction by A3, A4, A6, A7, A11, A35, SPPOL_1:7, TOPREAL1:6; :: thesis:

end;

A38: j + 1 >= i1 by A21, TOPREAL1:def 7;
then ( i1 + 1 = j or i1 = j or j + 1 = i1 ) by A30, A22, XXREAL_0:1;
then i1 <= j by A36, NAT_1:11;
hence i1 <= i2 by A29, XXREAL_0:2; :: thesis:
assume A39: i1 = i2 ; :: thesis:
not p in LSeg ((f /. j),q) by A4, A11, Th6;
then not LE p,q,f /. j,f /. (j + 1) by JORDAN3:30;
then LT q,p,f /. j,f /. (j + 1) by A3, A6, A13, A23, A30, A22, A38, A35, A36, A39, JORDAN3:28, XXREAL_0:1;
hence LE q,p,f /. i1,f /. (i1 + 1) by A23, A30, A22, A38, A36, A39, JORDAN3:def 6, XXREAL_0:1; :: thesis:

end;

hence LE q,p, L~ f,f /. 1,f /. (len f) by A3, A9, A10, A11, JORDAN5C:30; :: thesis:

end;

end;