let f be FinSequence of (); :: thesis: for q1, q2 being Point of ()
for i being Nat st q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) holds
LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)

let q1, q2 be Point of (); :: thesis: for i being Nat st q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) holds
LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)

let i be Nat; :: thesis: ( q1 in LSeg (f,i) & q2 in LSeg (f,i) & f is being_S-Seq & 1 <= i & i + 1 <= len f & LE q1,q2, L~ f,f /. 1,f /. (len f) implies LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) )
assume that
A1: q1 in LSeg (f,i) and
A2: q2 in LSeg (f,i) and
A3: f is being_S-Seq and
A4: ( 1 <= i & i + 1 <= len f ) ; :: thesis: ( not LE q1,q2, L~ f,f /. 1,f /. (len f) or LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) )
len f >= 2 by ;
then reconsider P = L~ f, Q = LSeg (f,i) as non empty Subset of () by ;
L~ f is_an_arc_of f /. 1,f /. (len f) by ;
then consider F being Function of I,(() | P) such that
A5: ( F is being_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) ) by TOPREAL1:def 1;
consider ppi, pi1 being Real such that
A6: ppi < pi1 and
A7: 0 <= ppi and
ppi <= 1 and
0 <= pi1 and
A8: pi1 <= 1 and
A9: LSeg (f,i) = F .: [.ppi,pi1.] and
A10: F . ppi = f /. i and
A11: F . pi1 = f /. (i + 1) by ;
set Ex = L (((#) (ppi,pi1)),((ppi,pi1) (#)));
A12: L (((#) (ppi,pi1)),((ppi,pi1) (#))) is being_homeomorphism by ;
then A13: rng (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) = [#] (Closed-Interval-TSpace (ppi,pi1)) by TOPS_2:def 5;
A14: ppi in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A6;
then reconsider Poz = [.ppi,pi1.] as non empty Subset of I by ;
consider G being Function of (I | Poz),(() | Q) such that
A15: G = F | Poz and
A16: G is being_homeomorphism by ;
A17: ppi in [.ppi,pi1.] by ;
set H = G * (L (((#) (ppi,pi1)),((ppi,pi1) (#))));
A18: dom G = [#] (I | Poz) by
.= Poz by PRE_TOPC:def 5
.= [#] (Closed-Interval-TSpace (ppi,pi1)) by ;
then A19: rng (G * (L (((#) (ppi,pi1)),((ppi,pi1) (#))))) = rng G by
.= [#] (() | (LSeg (f,i))) by ;
pi1 in { dd where dd is Real : ( ppi <= dd & dd <= pi1 ) } by A6;
then A20: pi1 in [.ppi,pi1.] by RCOMP_1:def 1;
A21: (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . 1 = (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . ((0,1) (#)) by TREAL_1:def 2
.= (ppi,pi1) (#) by
.= pi1 by ;
A22: dom (G * (L (((#) (ppi,pi1)),((ppi,pi1) (#))))) = dom (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) by
.= [#] I by
.= the carrier of I ;
then reconsider H = G * (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) as Function of I,(() | Q) by ;
q1 in rng H by ;
then consider x19 being object such that
A23: x19 in dom H and
A24: q1 = H . x19 by FUNCT_1:def 3;
x19 in { l where l is Real : ( 0 <= l & l <= 1 ) } by ;
then consider x1 being Real such that
A25: x1 = x19 and
A26: ( 0 <= x1 & x1 <= 1 ) ;
assume A27: LE q1,q2, L~ f,f /. 1,f /. (len f) ; :: thesis: LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1)
x1 in the carrier of I by ;
then x1 in dom (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) by ;
then (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1 in the carrier of (Closed-Interval-TSpace (ppi,pi1)) by ;
then A28: (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1 in Poz by ;
1 in dom H by ;
then A29: H . 1 = G . pi1 by
.= f /. (i + 1) by ;
A30: (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . 0 = (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . ((#) (0,1)) by TREAL_1:def 1
.= (#) (ppi,pi1) by
.= ppi by ;
q2 in rng H by ;
then consider x29 being object such that
A31: x29 in dom H and
A32: q2 = H . x29 by FUNCT_1:def 3;
x29 in { l where l is Real : ( 0 <= l & l <= 1 ) } by ;
then consider x2 being Real such that
A33: x2 = x29 and
A34: 0 <= x2 and
A35: x2 <= 1 ;
reconsider X1 = x1, X2 = x2 as Point of () by ;
x2 in the carrier of I by ;
then x2 in dom (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) by ;
then (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2 in the carrier of (Closed-Interval-TSpace (ppi,pi1)) by ;
then A36: (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2 in Poz by ;
then reconsider E1 = (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . X1, E2 = (L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . X2 as Real by A28;
A37: q2 = G . ((L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2) by
.= F . ((L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x2) by ;
reconsider K1 = Closed-Interval-TSpace (ppi,pi1), K2 = I | Poz as SubSpace of I by ;
A38: ( L (((#) (ppi,pi1)),((ppi,pi1) (#))) is one-to-one & L (((#) (ppi,pi1)),((ppi,pi1) (#))) is continuous ) by ;
the carrier of K1 = [.ppi,pi1.] by
.= [#] (I | Poz) by PRE_TOPC:def 5
.= the carrier of K2 ;
then I | Poz = Closed-Interval-TSpace (ppi,pi1) by TSEP_1:5;
then A39: H is being_homeomorphism by ;
A40: q1 = G . ((L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1) by
.= F . ((L (((#) (ppi,pi1)),((ppi,pi1) (#)))) . x1) by ;
A41: ( 0 <= E2 & E2 <= 1 ) by ;
0 in dom H by ;
then A42: H . 0 = G . ppi by
.= f /. i by ;
E1 <= 1 by ;
then E1 <= E2 by A27, A5, A40, A37, A41;
then x1 <= x2 by ;
hence LE q1,q2, LSeg (f,i),f /. i,f /. (i + 1) by A3, A4, A39, A42, A29, A24, A32, A25, A26, A33, A35, Th8, JORDAN5B:15; :: thesis: verum