let j be Element of NAT ; :: thesis: for f being S-Sequence_in_R2
for p, q being Point of (TOP-REAL 2) st 1 <= j & j < len f & p in LSeg f,j & q in LSeg (f /. j),p holds
LE q,p, L~ f,f /. 1,f /. (len f)
let f be S-Sequence_in_R2; :: thesis: for p, q being Point of (TOP-REAL 2) st 1 <= j & j < len f & p in LSeg f,j & q in LSeg (f /. j),p holds
LE q,p, L~ f,f /. 1,f /. (len f)
let p, q be Point of (TOP-REAL 2); :: thesis: ( 1 <= j & j < len f & p in LSeg f,j & q in LSeg (f /. j),p implies LE q,p, L~ f,f /. 1,f /. (len f) )
assume that
A1: ( 1 <= j & j < len f ) and
A2: p in LSeg f,j and
A3: q in LSeg (f /. j),p ; :: thesis: LE q,p, L~ f,f /. 1,f /. (len f)
A4: j + 1 <= len f by A1, NAT_1:13;
then A5: LSeg f,j = LSeg (f /. j),(f /. (j + 1)) by A1, TOPREAL1:def 5;
A6: f /. j in LSeg f,j by A1, A4, TOPREAL1:27;
then A7: LSeg (f /. j),p c= LSeg f,j by A2, A5, TOPREAL1:12;
then A8: q in LSeg f,j by A3;
A9: LSeg f,j c= L~ f by TOPREAL3:26;

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

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

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

end;

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

for i, j being Element of 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) ) )

proof

let i1, i2 be Element of NAT ; :: thesis: ( q in LSeg f,i1 & p in LSeg f,i2 & 1 <= i1 & i1 + 1 <= len f & 1 <= i2 & i2 + 1 <= len f implies ( i1 <= i2 & ( i1 = i2 implies LE q,p,f /. i1,f /. (i1 + 1) ) ) )
assume that
A11: q in LSeg f,i1 and
A12: p in LSeg f,i2 and
A13: ( 1 <= i1 & i1 + 1 <= len f ) and
A14: ( 1 <= i2 & i2 + 1 <= len f ) ; :: thesis: ( i1 <= i2 & ( i1 = i2 implies LE q,p,f /. i1,f /. (i1 + 1) ) )

A15: now

assume ( i2 + 1 > j & j + 1 > i2 ) ; :: thesis: i2 = j
then ( i2 <= j & j <= i2 ) by NAT_1:13;
hence i2 = j by XXREAL_0:1; :: thesis: verum

end;

A16: p in (LSeg f,i2) /\ (LSeg f,j) by A2, A12, XBOOLE_0:def 4;
then LSeg f,i2 meets LSeg f,j by XBOOLE_0:4;
then ( i2 + 1 >= j & j + 1 >= i2 ) by TOPREAL1:def 9;
then A17: ( i2 + 1 = j or i2 = j or j + 1 = i2 ) by A15, XXREAL_0:1;

A18: now

assume A19: i2 + 1 = j ; :: thesis: contradiction
i2 + (1 + 1) = (i2 + 1) + 1 ;
then i2 + 2 <= len f by A1, A19, NAT_1:13;
then p in {(f /. j)} by A14, A16, A19, TOPREAL1:def 8;
then p = f /. j by TARSKI:def 1;
then q in {p} by A3, RLTOPSP1:71;
hence contradiction by A10, TARSKI:def 1; :: thesis: verum

end;

then A20: i2 >= j by A17, NAT_1:11;

A21: now

assume ( i1 + 1 > j & j + 1 > i1 ) ; :: thesis: i1 = j
then ( i1 <= j & j <= i1 ) by NAT_1:13;
hence i1 = j by XXREAL_0:1; :: thesis: verum

end;

A22: q in (LSeg f,i1) /\ (LSeg f,j) by A3, A7, A11, XBOOLE_0:def 4;
then LSeg f,i1 meets LSeg f,j by XBOOLE_0:4;
then A23: ( i1 + 1 >= j & j + 1 >= i1 ) by TOPREAL1:def 9;
then A24: ( i1 + 1 = j or i1 = j or j + 1 = i1 ) by A21, XXREAL_0:1;
1 <= j + 1 by NAT_1:11;
then A25: j + 1 in dom f by A4, FINSEQ_3:27;
A26: j in dom f by A1, FINSEQ_3:27;

A27: now

assume f /. (j + 1) = f /. j ; :: thesis: contradiction
then j = j + 1 by A25, A26, PARTFUN2:17;
hence contradiction ; :: thesis: verum

end;

A28: now

assume A29: i1 = j + 1 ; :: thesis: contradiction
j + (1 + 1) = (j + 1) + 1 ;
then q in {(f /. (j + 1))} by A1, A13, A22, A29, TOPREAL1:def 8;
then q = f /. (j + 1) by TARSKI:def 1;
hence contradiction by A2, A3, A5, A6, A10, A27, SPPOL_1:24, TOPREAL1:12; :: thesis: verum

end;

then i1 <= j by A24, NAT_1:11;
hence i1 <= i2 by A20, XXREAL_0:2; :: thesis: ( i1 = i2 implies LE q,p,f /. i1,f /. (i1 + 1) )
assume A30: i1 = i2 ; :: thesis: LE q,p,f /. i1,f /. (i1 + 1)
not p in LSeg (f /. j),q by A3, A10, Th16;
then not LE p,q,f /. j,f /. (j + 1) by JORDAN3:65;
then LT q,p,f /. j,f /. (j + 1) by A2, A5, A11, A18, A21, A23, A27, A28, A30, JORDAN3:63, XXREAL_0:1;
hence LE q,p,f /. i1,f /. (i1 + 1) by A18, A21, A23, A28, A30, JORDAN3:def 7, XXREAL_0:1; :: thesis: verum

end;

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

end;

end;