let f be FinSequence of (TOP-REAL 2); :: thesis:
let q1, q2 be Point of (TOP-REAL 2); :: thesis:
set p3 = f /. 1;
set p4 = f /. (len f);
assume A1: ( q1 in L~ f & q2 in L~ f & f is being_S-Seq & q1 <> q2 ) ; :: thesis:
then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) ;

hereby :: thesis:

assume A2: LE q1,q2, L~ f,f /. 1,f /. (len f) ; :: thesis:
thus for i, j being Element of NAT st q1 in LSeg f,i & q2 in LSeg f,j & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) :: thesis:

proof

let i, j be Element of NAT ; :: thesis:
assume A3: ( q1 in LSeg f,i & q2 in LSeg f,j & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f ) ; :: thesis:
thus i <= j :: thesis:

proof

assume j < i ; :: thesis:
then j + 1 <= i by NAT_1:13;
then consider m being Nat such that
A4: (j + 1) + m = i by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A5: LE q2,f /. (j + 1),P,f /. 1,f /. (len f) by A1, A3, Th26;
( i <= i + 1 & j <= j + 1 ) by NAT_1:11;
then ( 1 <= j + 1 & j + 1 <= (j + 1) + m & (j + 1) + m <= len f ) by A3, A4, NAT_1:11, XXREAL_0:2;
then LE f /. (j + 1),f /. ((j + 1) + m),P,f /. 1,f /. (len f) by A1, Th24;
then A6: LE q2,f /. ((j + 1) + m),P,f /. 1,f /. (len f) by A5, Th13;
LE f /. ((j + 1) + m),q1,P,f /. 1,f /. (len f) by A1, A3, A4, Th25;
then LE q2,q1,P,f /. 1,f /. (len f) by A6, Th13;
hence contradiction by A1, A2, Th12, TOPREAL1:31; :: thesis:

end;

assume A7: i = j ; :: thesis:
set p1 = f /. i;
set p2 = f /. (i + 1);
A8: ( i in dom f & i + 1 in dom f ) by A3, GOBOARD2:3;
A9: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A3, TOPREAL1:def 5;
A10: f is one-to-one by A1, TOPREAL1:def 10;
f /. i <> f /. (i + 1)

proof

assume f /. i = f /. (i + 1) ; :: thesis:
then i = i + 1 by A8, A10, PARTFUN2:17;
hence contradiction ; :: thesis:

end;

hence LE q1,q2,f /. i,f /. (i + 1) by A1, A2, A3, A7, A9, Th17, Th29; :: thesis:

end;

assume A11: for i, j being Element of NAT st q1 in LSeg f,i & q2 in LSeg f,j & 1 <= i & i + 1 <= len f & 1 <= j & j + 1 <= len f holds
( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) ; :: thesis:
consider i being Element of NAT such that
A12: ( 1 <= i & i + 1 <= len f & q1 in LSeg f,i ) by A1, SPPOL_2:13;
consider j being Element of NAT such that
A13: ( 1 <= j & j + 1 <= len f & q2 in LSeg f,j ) by A1, SPPOL_2:13;
A14: ( i <= j & ( i = j implies LE q1,q2,f /. i,f /. (i + 1) ) ) by A11, A12, A13;

per cases by A14, XXREAL_0:1;

suppose i < j ; :: thesis:

then i + 1 <= j by NAT_1:13;
then consider m being Nat such that
A15: j = (i + 1) + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A16: ( 1 <= i + 1 & ((i + 1) + m) + 1 <= len f ) by A13, A15, NAT_1:12;
A17: LE q1,f /. (i + 1),P,f /. 1,f /. (len f) by A1, A12, Th26;
( i <= i + 1 & j <= j + 1 ) by NAT_1:11;
then ( i + 1 <= (i + 1) + m & (i + 1) + m <= len f ) by A13, A15, NAT_1:11, XXREAL_0:2;
then LE f /. (i + 1),f /. ((i + 1) + m),P,f /. 1,f /. (len f) by A1, A16, Th24;
then A18: LE q1,f /. ((i + 1) + m),P,f /. 1,f /. (len f) by A17, Th13;
LE f /. ((i + 1) + m),q2,P,f /. 1,f /. (len f) by A1, A13, A15, Th25;
hence LE q1,q2, L~ f,f /. 1,f /. (len f) by A18, Th13; :: thesis:

end;

suppose A19: i = j ; :: thesis:

then A20: LE q1,q2,f /. i,f /. (i + 1) by A11, A12, A13;
set p1 = f /. i;
set p2 = f /. (i + 1);
A21: ( i in dom f & i + 1 in dom f ) by A12, GOBOARD2:3;
A22: f is one-to-one by A1, TOPREAL1:def 10;
f /. i <> f /. (i + 1)

proof

assume f /. i = f /. (i + 1) ; :: thesis:
then i = i + 1 by A21, A22, PARTFUN2:17;
hence contradiction ; :: thesis:

end;

then consider H being Function of I[01] ,((TOP-REAL 2) | (LSeg (f /. i),(f /. (i + 1)))) such that
A23: ( ( for x being Real st x in [.0 ,1.] holds
H . x = ((1 - x) * (f /. i)) + (x * (f /. (i + 1))) ) & H is being_homeomorphism & H . 0 = f /. i & H . 1 = f /. (i + 1) ) by JORDAN5A:4;
A24: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A12, TOPREAL1:def 5;
reconsider Q = LSeg f,i as non empty Subset of (TOP-REAL 2) by A12;
reconsider H = H as Function of I[01] ,((TOP-REAL 2) | Q) by A24;
( q1 in P & q2 in P & ( for g being Function of I[01] ,((TOP-REAL 2) | P)
for s1, s2 being Real st g is being_homeomorphism & g . 0 = f /. 1 & g . 1 = f /. (len f) & g . s1 = q1 & 0 <= s1 & s1 <= 1 & g . s2 = q2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2 ) )

proof

thus ( q1 in P & q2 in P ) by A1; :: thesis:
let F be Function of I[01] ,((TOP-REAL 2) | P); :: thesis:
let s1, s2 be Real; :: thesis:
assume A25: ( F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & F . s1 = q1 & 0 <= s1 & s1 <= 1 & F . s2 = q2 & 0 <= s2 & s2 <= 1 ) ; :: thesis:
then A26: ( s1 in the carrier of I[01] & s2 in the carrier of I[01] ) by BORSUK_1:86;
A27: dom F = [#] I[01] by A25, TOPS_2:def 5
.= the carrier of I[01] ;
A28: F is one-to-one by A25, TOPS_2:def 5;
consider ppi, pi1 being Real such that
A29: ( ppi < pi1 & 0 <= ppi & ppi <= 1 & 0 <= pi1 & pi1 <= 1 & LSeg f,i = F .: [.ppi,pi1.] & F . ppi = f /. i & F . pi1 = f /. (i + 1) ) by A1, A12, A25, JORDAN5B:7;
A30: ( ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } & pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } ) by A29;
then A31: ( ppi in [.ppi,pi1.] & pi1 in [.ppi,pi1.] ) by RCOMP_1:def 1;
reconsider Poz = [.ppi,pi1.] as non empty Subset of I[01] by A29, A30, BORSUK_1:83, RCOMP_1:def 1, XXREAL_1:34;
consider G being Function of (I[01] | Poz),((TOP-REAL 2) | Q) such that
A32: ( G = F | Poz & G is being_homeomorphism ) by A1, A12, A25, A29, JORDAN5B:8;
A33: dom H = [#] I[01] by A23, TOPS_2:def 5
.= [.0 ,1.] by BORSUK_1:83 ;
A34: rng H = [#] ((TOP-REAL 2) | (LSeg f,i)) by A23, A24, TOPS_2:def 5
.= LSeg f,i by PRE_TOPC:def 10 ;
then consider x1' being set such that
A35: ( x1' in dom H & H . x1' = q1 ) by A12, FUNCT_1:def 5;
x1' in { l where l is Real : ( 0 <= l & l <= 1 ) } by A33, A35, RCOMP_1:def 1;
then consider x1 being Real such that
A36: ( x1 = x1' & 0 <= x1 & x1 <= 1 ) ;
consider x2' being set such that
A37: ( x2' in dom H & H . x2' = q2 ) by A13, A19, A34, FUNCT_1:def 5;
x2' in { l where l is Real : ( 0 <= l & l <= 1 ) } by A33, A37, RCOMP_1:def 1;
then consider x2 being Real such that
A38: ( x2 = x2' & 0 <= x2 & x2 <= 1 ) ;
reconsider K1 = Closed-Interval-TSpace ppi,pi1, K2 = I[01] | Poz as SubSpace of I[01] by A29, TOPMETR:27, TREAL_1:6;
A39: the carrier of K1 = [.ppi,pi1.] by A29, TOPMETR:25
.= [#] (I[01] | Poz) by PRE_TOPC:def 10
.= the carrier of K2 ;
then A40: Closed-Interval-TSpace ppi,pi1 = I[01] | Poz by TSEP_1:5;
reconsider E = (G " ) * H as Function of (Closed-Interval-TSpace 0 ,1),(Closed-Interval-TSpace ppi,pi1) by A39, TOPMETR:27;
( G " is being_homeomorphism & H is being_homeomorphism ) by A23, A24, A32, TOPS_2:70;
then E is being_homeomorphism by A40, TOPMETR:27, TOPS_2:71;
then A41: ( E is continuous & E is one-to-one ) by TOPS_2:def 5;
A42: ( dom G = [#] (I[01] | Poz) & rng G = [#] ((TOP-REAL 2) | (LSeg f,i)) & G is one-to-one ) by A32, TOPS_2:def 5;
then A43: dom G = Poz by PRE_TOPC:def 10;
A44: G " = G " by A42, TOPS_2:def 4;
( 0 in { l where l is Real : ( 0 <= l & l <= 1 ) } & 1 in { l where l is Real : ( 0 <= l & l <= 1 ) } ) ;
then A45: ( 0 in [.0 ,1.] & 1 in [.0 ,1.] ) by RCOMP_1:def 1;
then A46: H . 0 = ((1 - 0 ) * (f /. i)) + (0 * (f /. (i + 1))) by A23
.= (f /. i) + (0 * (f /. (i + 1))) by EUCLID:33
.= (f /. i) + (0. (TOP-REAL 2)) by EUCLID:33
.= f /. i by EUCLID:31 ;
A47: H . 1 = ((1 - 1) * (f /. i)) + (1 * (f /. (i + 1))) by A23, A45
.= (0. (TOP-REAL 2)) + (1 * (f /. (i + 1))) by EUCLID:33
.= (0. (TOP-REAL 2)) + (f /. (i + 1)) by EUCLID:33
.= f /. (i + 1) by EUCLID:31 ;
G . ppi = f /. i by A29, A31, A32, FUNCT_1:72;
then A48: ppi = (G " ) . (H . 0 ) by A31, A42, A43, A44, A46, FUNCT_1:54
.= E . 0 by A33, A45, FUNCT_1:23 ;
G . pi1 = f /. (i + 1) by A29, A31, A32, FUNCT_1:72;
then A49: pi1 = (G " ) . (H . 1) by A31, A42, A43, A44, A47, FUNCT_1:54
.= E . 1 by A33, A45, FUNCT_1:23 ;
consider x being set such that
A50: ( x in dom F & x in [.ppi,pi1.] & q1 = F . x ) by A12, A29, FUNCT_1:def 12;
A51: x = s1 by A25, A26, A27, A28, A50, FUNCT_1:def 8;
A52: s1 in dom G by A25, A26, A27, A28, A43, A50, FUNCT_1:def 8;
G . s1 = q1 by A32, A50, A51, FUNCT_1:72;
then A53: s1 = (G " ) . (H . x1) by A35, A36, A42, A44, A52, FUNCT_1:54
.= E . x1 by A35, A36, FUNCT_1:23 ;
consider x' being set such that
A54: ( x' in dom F & x' in [.ppi,pi1.] & q2 = F . x' ) by A13, A19, A29, FUNCT_1:def 12;
A55: s2 in Poz by A25, A26, A27, A28, A54, FUNCT_1:def 8;
A56: s2 in dom G by A25, A26, A27, A28, A43, A54, FUNCT_1:def 8;
G . s2 = q2 by A25, A32, A55, FUNCT_1:72;
then A57: s2 = (G " ) . (H . x2) by A37, A38, A42, A44, A56, FUNCT_1:54
.= E . x2 by A37, A38, FUNCT_1:23 ;
reconsider X1 = x1, X2 = x2 as Point of (Closed-Interval-TSpace 0 ,1) by A33, A35, A36, A37, A38, TOPMETR:25;
A58: ( s1 = E . X1 & s2 = E . X2 ) by A53, A57;
A59: q1 = ((1 - x1) * (f /. i)) + (x1 * (f /. (i + 1))) by A23, A33, A35, A36;
q2 = ((1 - x2) * (f /. i)) + (x2 * (f /. (i + 1))) by A23, A33, A37, A38;
then A60: x1 <= x2 by A20, A36, A38, A59, JORDAN3:def 6;

per cases by A60, XXREAL_0:1;

suppose x1 = x2 ; :: thesis:

hence s1 <= s2 by A53, A57; :: thesis:

end;

suppose x1 < x2 ; :: thesis:

hence s1 <= s2 by A29, A41, A48, A49, A58, JORDAN5A:16; :: thesis:

end;

hence LE q1,q2, L~ f,f /. 1,f /. (len f) by Def3; :: thesis:

end;