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

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

LE p,q, L~ f,f /. 1,f /. (len f)

let p, q be Point of (TOP-REAL 2); :: thesis: for j being Nat st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg (p,(f /. (j + 1))) holds

LE p,q, L~ f,f /. 1,f /. (len f)

let j be Nat; :: thesis: ( 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg (p,(f /. (j + 1))) implies LE p,q, L~ f,f /. 1,f /. (len f) )

assume that

A1: 1 <= j and

A2: j < len f and

A3: p in LSeg (f,j) and

A4: q in LSeg (p,(f /. (j + 1))) ; :: thesis: LE p,q, L~ f,f /. 1,f /. (len f)

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 + 1) in LSeg (f,j) by A1, A5, TOPREAL1:21;

then A8: LSeg (p,(f /. (j + 1))) 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;

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

LE p,q, L~ f,f /. 1,f /. (len f)

let p, q be Point of (TOP-REAL 2); :: thesis: for j being Nat st 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg (p,(f /. (j + 1))) holds

LE p,q, L~ f,f /. 1,f /. (len f)

let j be Nat; :: thesis: ( 1 <= j & j < len f & p in LSeg (f,j) & q in LSeg (p,(f /. (j + 1))) implies LE p,q, L~ f,f /. 1,f /. (len f) )

assume that

A1: 1 <= j and

A2: j < len f and

A3: p in LSeg (f,j) and

A4: q in LSeg (p,(f /. (j + 1))) ; :: thesis: LE p,q, L~ f,f /. 1,f /. (len f)

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 + 1) in LSeg (f,j) by A1, A5, TOPREAL1:21;

then A8: LSeg (p,(f /. (j + 1))) 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;

per cases
( p = q or q <> p )
;

end;

suppose A11:
q <> p
; :: thesis: LE p,q, L~ f,f /. 1,f /. (len f)

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

( i <= j & ( i = j implies LE p,q,f /. i,f /. (i + 1) ) )

end;( i <= j & ( i = j implies LE p,q,f /. i,f /. (i + 1) ) )

proof

hence
LE p,q, L~ f,f /. 1,f /. (len f)
by A3, A9, A10, A11, JORDAN5C:30; :: thesis: verum
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: ( p in LSeg (f,i1) & q in LSeg (f,i2) & 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f implies ( i1 <= i2 & ( i1 = i2 implies LE p,q,f /. i1,f /. (i1 + 1) ) ) )

assume that

A13: p in LSeg (f,i1) and

A14: q in LSeg (f,i2) and

1 <= i1 and

A15: i1 + 1 <= len f and

A16: 1 <= i2 and

i2 + 1 <= len f ; :: thesis: ( i1 <= i2 & ( i1 = i2 implies LE p,q,f /. i1,f /. (i1 + 1) ) )

A17: p in (LSeg (f,i1)) /\ (LSeg (f,j)) by A3, A13, XBOOLE_0:def 4;

then A18: LSeg (f,i1) meets LSeg (f,j) by XBOOLE_0:4;

then A19: i1 + 1 >= j by TOPREAL1:def 7;

then A31: LSeg (f,i2) meets LSeg (f,j) by XBOOLE_0:4;

then A32: j + 1 >= i2 by TOPREAL1:def 7;

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

then ( i2 + 1 = j or i2 = j or j + 1 = i2 ) by A22, A32, XXREAL_0:1;

then A37: i2 >= j by A35, NAT_1:11;

A38: j + 1 >= i1 by A18, TOPREAL1:def 7;

then ( i1 + 1 = j or i1 = j ) by A26, A19, A20, XXREAL_0:1;

then i1 <= j by NAT_1:11;

hence i1 <= i2 by A37, XXREAL_0:2; :: thesis: ( i1 = i2 implies LE p,q,f /. i1,f /. (i1 + 1) )

assume A39: i1 = i2 ; :: thesis: LE p,q,f /. i1,f /. (i1 + 1)

not p in LSeg (q,(f /. (j + 1))) by A4, A11, SPRECT_3:6;

then not LE q,p,f /. j,f /. (j + 1) by JORDAN3:30;

then LT p,q,f /. j,f /. (j + 1) by A3, A6, A14, A26, A19, A38, A20, A34, A35, A39, JORDAN3:28, XXREAL_0:1;

hence LE p,q,f /. i1,f /. (i1 + 1) by A26, A19, A38, A20, A35, A39, JORDAN3:def 6, XXREAL_0:1; :: thesis: verum

end;then A12: j + 1 in dom f by A5, FINSEQ_3:25;

let i1, i2 be Nat; :: thesis: ( p in LSeg (f,i1) & q in LSeg (f,i2) & 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f implies ( i1 <= i2 & ( i1 = i2 implies LE p,q,f /. i1,f /. (i1 + 1) ) ) )

assume that

A13: p in LSeg (f,i1) and

A14: q in LSeg (f,i2) and

1 <= i1 and

A15: i1 + 1 <= len f and

A16: 1 <= i2 and

i2 + 1 <= len f ; :: thesis: ( i1 <= i2 & ( i1 = i2 implies LE p,q,f /. i1,f /. (i1 + 1) ) )

A17: p in (LSeg (f,i1)) /\ (LSeg (f,j)) by A3, A13, XBOOLE_0:def 4;

then A18: LSeg (f,i1) meets LSeg (f,j) by XBOOLE_0:4;

then A19: i1 + 1 >= j by TOPREAL1:def 7;

A20: now :: thesis: not j + 1 = i1

A21:
j + (1 + 1) = (j + 1) + 1
;

assume j + 1 = i1 ; :: thesis: contradiction

then p in {(f /. (j + 1))} by A1, A15, A17, A21, TOPREAL1:def 6;

then p = f /. (j + 1) by TARSKI:def 1;

then q in {p} by A4, RLTOPSP1:70;

hence contradiction by A11, TARSKI:def 1; :: thesis: verum

end;assume j + 1 = i1 ; :: thesis: contradiction

then p in {(f /. (j + 1))} by A1, A15, A17, A21, TOPREAL1:def 6;

then p = f /. (j + 1) by TARSKI:def 1;

then q in {p} by A4, RLTOPSP1:70;

hence contradiction by A11, TARSKI:def 1; :: thesis: verum

A22: now :: thesis: ( i2 + 1 > j & j + 1 > i2 implies i2 = j )

assume that

A23: i2 + 1 > j and

A24: j + 1 > i2 ; :: thesis: i2 = j

A25: j <= i2 by A23, NAT_1:13;

i2 <= j by A24, NAT_1:13;

hence i2 = j by A25, XXREAL_0:1; :: thesis: verum

end;A23: i2 + 1 > j and

A24: j + 1 > i2 ; :: thesis: i2 = j

A25: j <= i2 by A23, NAT_1:13;

i2 <= j by A24, NAT_1:13;

hence i2 = j by A25, XXREAL_0:1; :: thesis: verum

A26: now :: thesis: ( i1 + 1 > j & j + 1 > i1 implies i1 = j )

A30:
q in (LSeg (f,i2)) /\ (LSeg (f,j))
by A4, A8, A14, XBOOLE_0:def 4;assume that

A27: i1 + 1 > j and

A28: j + 1 > i1 ; :: thesis: i1 = j

A29: j <= i1 by A27, NAT_1:13;

i1 <= j by A28, NAT_1:13;

hence i1 = j by A29, XXREAL_0:1; :: thesis: verum

end;A27: i1 + 1 > j and

A28: j + 1 > i1 ; :: thesis: i1 = j

A29: j <= i1 by A27, NAT_1:13;

i1 <= j by A28, NAT_1:13;

hence i1 = j by A29, XXREAL_0:1; :: thesis: verum

then A31: LSeg (f,i2) meets LSeg (f,j) by XBOOLE_0:4;

then A32: j + 1 >= i2 by TOPREAL1:def 7;

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

A34: now :: thesis: not f /. (j + 1) = f /. j

assume
f /. (j + 1) = f /. j
; :: thesis: contradiction

then j = j + 1 by A12, A33, PARTFUN2:10;

hence contradiction ; :: thesis: verum

end;then j = j + 1 by A12, A33, PARTFUN2:10;

hence contradiction ; :: thesis: verum

A35: now :: thesis: not i2 + 1 = j

i2 + 1 >= j
by A31, TOPREAL1:def 7;A36:
i2 + (1 + 1) = (i2 + 1) + 1
;

assume i2 + 1 = j ; :: thesis: contradiction

then q in {(f /. j)} by A5, A16, A30, A36, TOPREAL1:def 6;

then q = f /. j by TARSKI:def 1;

hence contradiction by A3, A4, A6, A7, A11, A34, SPPOL_1:7, TOPREAL1:6; :: thesis: verum

end;assume i2 + 1 = j ; :: thesis: contradiction

then q in {(f /. j)} by A5, A16, A30, A36, TOPREAL1:def 6;

then q = f /. j by TARSKI:def 1;

hence contradiction by A3, A4, A6, A7, A11, A34, SPPOL_1:7, TOPREAL1:6; :: thesis: verum

then ( i2 + 1 = j or i2 = j or j + 1 = i2 ) by A22, A32, XXREAL_0:1;

then A37: i2 >= j by A35, NAT_1:11;

A38: j + 1 >= i1 by A18, TOPREAL1:def 7;

then ( i1 + 1 = j or i1 = j ) by A26, A19, A20, XXREAL_0:1;

then i1 <= j by NAT_1:11;

hence i1 <= i2 by A37, XXREAL_0:2; :: thesis: ( i1 = i2 implies LE p,q,f /. i1,f /. (i1 + 1) )

assume A39: i1 = i2 ; :: thesis: LE p,q,f /. i1,f /. (i1 + 1)

not p in LSeg (q,(f /. (j + 1))) by A4, A11, SPRECT_3:6;

then not LE q,p,f /. j,f /. (j + 1) by JORDAN3:30;

then LT p,q,f /. j,f /. (j + 1) by A3, A6, A14, A26, A19, A38, A20, A34, A35, A39, JORDAN3:28, XXREAL_0:1;

hence LE p,q,f /. i1,f /. (i1 + 1) by A26, A19, A38, A20, A35, A39, JORDAN3:def 6, XXREAL_0:1; :: thesis: verum