let f be S-Sequence_in_R2; :: thesis: for p, q being Point of ()
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 (); :: 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 ;
then A6: LSeg (f,j) = LSeg ((f /. j),(f /. (j + 1))) by ;
A7: f /. (j + 1) in LSeg (f,j) by ;
then A8: LSeg (p,(f /. (j + 1))) c= LSeg (f,j) by ;
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 ) ;
suppose p = q ; :: thesis: LE p,q, L~ f,f /. 1,f /. (len f)
hence LE p,q, L~ f,f /. 1,f /. (len f) by ; :: thesis: verum
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) ) )
proof
1 <= j + 1 by NAT_1:11;
then A12: j + 1 in dom f by ;
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 ;
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 ;
then p = f /. (j + 1) by TARSKI:def 1;
then q in {p} by ;
hence contradiction by A11, TARSKI:def 1; :: thesis: verum
end;
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 ;
i2 <= j by ;
hence i2 = j by ; :: thesis: verum
end;
A26: now :: thesis: ( i1 + 1 > j & j + 1 > i1 implies i1 = j )
assume that
A27: i1 + 1 > j and
A28: j + 1 > i1 ; :: thesis: i1 = j
A29: j <= i1 by ;
i1 <= j by ;
hence i1 = j by ; :: thesis: verum
end;
A30: q in (LSeg (f,i2)) /\ (LSeg (f,j)) by ;
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 ;
A34: now :: thesis: not f /. (j + 1) = f /. j
assume f /. (j + 1) = f /. j ; :: thesis: contradiction
then j = j + 1 by ;
hence contradiction ; :: thesis: verum
end;
A35: now :: thesis: not i2 + 1 = j
A36: i2 + (1 + 1) = (i2 + 1) + 1 ;
assume i2 + 1 = j ; :: thesis: contradiction
then q in {(f /. j)} by ;
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;
i2 + 1 >= j by ;
then ( i2 + 1 = j or i2 = j or j + 1 = i2 ) by ;
then A37: i2 >= j by ;
A38: j + 1 >= i1 by ;
then ( i1 + 1 = j or i1 = j ) by ;
then i1 <= j by NAT_1:11;
hence i1 <= i2 by ; :: 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 ;
then not LE q,p,f /. j,f /. (j + 1) by JORDAN3:30;
then LT p,q,f /. j,f /. (j + 1) by ;
hence LE p,q,f /. i1,f /. (i1 + 1) by ; :: thesis: verum
end;
hence LE p,q, L~ f,f /. 1,f /. (len f) by ; :: thesis: verum
end;
end;