let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 holds

LE q2,q1,P,p2,p1

let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 implies LE q2,q1,P,p2,p1 )

assume that

A1: P is_an_arc_of p1,p2 and

A2: LE q1,q2,P,p1,p2 ; :: thesis: LE q2,q1,P,p2,p1

thus ( q2 in P & q1 in P ) by A2; :: according to JORDAN5C:def 3 :: thesis: for b_{1} being Element of K16(K17( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))

for b_{2}, b_{3} being object holds

( not b_{1} is being_homeomorphism or not b_{1} . 0 = p2 or not b_{1} . 1 = p1 or not b_{1} . b_{2} = q2 or not 0 <= b_{2} or not b_{2} <= 1 or not b_{1} . b_{3} = q1 or not 0 <= b_{3} or not b_{3} <= 1 or b_{2} <= b_{3} )

reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;

let f be Function of I[01],((TOP-REAL 2) | P); :: thesis: for b_{1}, b_{2} being object holds

( not f is being_homeomorphism or not f . 0 = p2 or not f . 1 = p1 or not f . b_{1} = q2 or not 0 <= b_{1} or not b_{1} <= 1 or not f . b_{2} = q1 or not 0 <= b_{2} or not b_{2} <= 1 or b_{1} <= b_{2} )

let s1, s2 be Real; :: thesis: ( not f is being_homeomorphism or not f . 0 = p2 or not f . 1 = p1 or not f . s1 = q2 or not 0 <= s1 or not s1 <= 1 or not f . s2 = q1 or not 0 <= s2 or not s2 <= 1 or s1 <= s2 )

assume that

A3: f is being_homeomorphism and

A4: f . 0 = p2 and

A5: f . 1 = p1 and

A6: f . s1 = q2 and

A7: 0 <= s1 and

A8: s1 <= 1 and

A9: f . s2 = q1 and

A10: 0 <= s2 and

A11: s2 <= 1 ; :: thesis: s1 <= s2

A12: 1 - 0 >= 1 - s1 by A7, XREAL_1:13;

A13: 1 - 0 >= 1 - s2 by A10, XREAL_1:13;

A14: 1 - 1 <= 1 - s1 by A8, XREAL_1:13;

A15: 1 - 1 <= 1 - s2 by A11, XREAL_1:13;

set Ex = L[01] (((0,1) (#)),((#) (0,1)));

A16: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18;

set g = f * (L[01] (((0,1) (#)),((#) (0,1))));

A17: (L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def 14, TREAL_1:5, TREAL_1:9;

A18: (L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def 15, TREAL_1:5, TREAL_1:9;

dom f = [#] I[01] by A3, TOPS_2:def 5;

then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A16, TOPMETR:20, TOPS_2:def 5;

then dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = dom (L[01] (((0,1) (#)),((#) (0,1)))) by RELAT_1:27;

then A19: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A16, TOPMETR:20, TOPS_2:def 5;

reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL 2) | P9) by TOPMETR:20;

A20: g is being_homeomorphism by A3, A16, TOPMETR:20, TOPS_2:57;

A21: 1 - s1 in dom g by A12, A14, A19, BORSUK_1:43;

A22: 1 - s2 in dom g by A13, A15, A19, BORSUK_1:43;

A23: g . 0 = p1 by A5, A18, A19, BORSUK_1:def 14, FUNCT_1:12, TREAL_1:5;

A24: g . 1 = p2 by A4, A17, A19, BORSUK_1:def 15, FUNCT_1:12, TREAL_1:5;

reconsider qs1 = 1 - s1, qs2 = 1 - s2 as Point of (Closed-Interval-TSpace (0,1)) by A12, A13, A14, A15, BORSUK_1:43, TOPMETR:20;

A25: (L[01] (((0,1) (#)),((#) (0,1)))) . qs1 = ((1 - (1 - s1)) * 1) + ((1 - s1) * 0) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5, TREAL_1:def 3

.= s1 ;

A26: (L[01] (((0,1) (#)),((#) (0,1)))) . qs2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5, TREAL_1:def 3

.= s2 ;

A27: g . (1 - s1) = q2 by A6, A21, A25, FUNCT_1:12;

g . (1 - s2) = q1 by A9, A22, A26, FUNCT_1:12;

then 1 - s2 <= 1 - s1 by A2, A12, A13, A14, A20, A23, A24, A27;

then s1 <= 1 - (1 - s2) by XREAL_1:11;

hence s1 <= s2 ; :: thesis: verum

LE q2,q1,P,p2,p1

let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 implies LE q2,q1,P,p2,p1 )

assume that

A1: P is_an_arc_of p1,p2 and

A2: LE q1,q2,P,p1,p2 ; :: thesis: LE q2,q1,P,p2,p1

thus ( q2 in P & q1 in P ) by A2; :: according to JORDAN5C:def 3 :: thesis: for b

for b

( not b

reconsider P9 = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;

let f be Function of I[01],((TOP-REAL 2) | P); :: thesis: for b

( not f is being_homeomorphism or not f . 0 = p2 or not f . 1 = p1 or not f . b

let s1, s2 be Real; :: thesis: ( not f is being_homeomorphism or not f . 0 = p2 or not f . 1 = p1 or not f . s1 = q2 or not 0 <= s1 or not s1 <= 1 or not f . s2 = q1 or not 0 <= s2 or not s2 <= 1 or s1 <= s2 )

assume that

A3: f is being_homeomorphism and

A4: f . 0 = p2 and

A5: f . 1 = p1 and

A6: f . s1 = q2 and

A7: 0 <= s1 and

A8: s1 <= 1 and

A9: f . s2 = q1 and

A10: 0 <= s2 and

A11: s2 <= 1 ; :: thesis: s1 <= s2

A12: 1 - 0 >= 1 - s1 by A7, XREAL_1:13;

A13: 1 - 0 >= 1 - s2 by A10, XREAL_1:13;

A14: 1 - 1 <= 1 - s1 by A8, XREAL_1:13;

A15: 1 - 1 <= 1 - s2 by A11, XREAL_1:13;

set Ex = L[01] (((0,1) (#)),((#) (0,1)));

A16: L[01] (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18;

set g = f * (L[01] (((0,1) (#)),((#) (0,1))));

A17: (L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by BORSUK_1:def 14, TREAL_1:5, TREAL_1:9;

A18: (L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by BORSUK_1:def 15, TREAL_1:5, TREAL_1:9;

dom f = [#] I[01] by A3, TOPS_2:def 5;

then rng (L[01] (((0,1) (#)),((#) (0,1)))) = dom f by A16, TOPMETR:20, TOPS_2:def 5;

then dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = dom (L[01] (((0,1) (#)),((#) (0,1)))) by RELAT_1:27;

then A19: dom (f * (L[01] (((0,1) (#)),((#) (0,1))))) = [#] I[01] by A16, TOPMETR:20, TOPS_2:def 5;

reconsider g = f * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],((TOP-REAL 2) | P9) by TOPMETR:20;

A20: g is being_homeomorphism by A3, A16, TOPMETR:20, TOPS_2:57;

A21: 1 - s1 in dom g by A12, A14, A19, BORSUK_1:43;

A22: 1 - s2 in dom g by A13, A15, A19, BORSUK_1:43;

A23: g . 0 = p1 by A5, A18, A19, BORSUK_1:def 14, FUNCT_1:12, TREAL_1:5;

A24: g . 1 = p2 by A4, A17, A19, BORSUK_1:def 15, FUNCT_1:12, TREAL_1:5;

reconsider qs1 = 1 - s1, qs2 = 1 - s2 as Point of (Closed-Interval-TSpace (0,1)) by A12, A13, A14, A15, BORSUK_1:43, TOPMETR:20;

A25: (L[01] (((0,1) (#)),((#) (0,1)))) . qs1 = ((1 - (1 - s1)) * 1) + ((1 - s1) * 0) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5, TREAL_1:def 3

.= s1 ;

A26: (L[01] (((0,1) (#)),((#) (0,1)))) . qs2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0) by BORSUK_1:def 14, BORSUK_1:def 15, TREAL_1:5, TREAL_1:def 3

.= s2 ;

A27: g . (1 - s1) = q2 by A6, A21, A25, FUNCT_1:12;

g . (1 - s2) = q1 by A9, A22, A26, FUNCT_1:12;

then 1 - s2 <= 1 - s1 by A2, A12, A13, A14, A20, A23, A24, A27;

then s1 <= 1 - (1 - s2) by XREAL_1:11;

hence s1 <= s2 ; :: thesis: verum