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 A1: ( P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 ) ; :: thesis: LE q2,q1,P,p2,p1
hence ( q2 in P & q1 in P ) by JORDAN5C:def 3; :: according to JORDAN5C:def 3 :: thesis: for b₁ being Element of K21(K22(the carrier of I[01] ,the carrier of ((TOP-REAL 2) | P)))
for b₂, b₃ being Element of REAL holds
( not b₁ is being_homeomorphism or not b₁ . 0 = p2 or not b₁ . 1 = p1 or not b₁ . b₂ = q2 or not 0 <= b₂ or not b₂ <= 1 or not b₁ . b₃ = q1 or not 0 <= b₃ or not b₃ <= 1 or b₂ <= b₃ )
reconsider P' = P as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:4;
let f be Function of I[01] ,((TOP-REAL 2) | P); :: thesis: for b₁, b₂ being Element of REAL holds
( not f is being_homeomorphism or not f . 0 = p2 or not f . 1 = p1 or not f . b₁ = q2 or not 0 <= b₁ or not b₁ <= 1 or not f . b₂ = q1 or not 0 <= b₂ or not b₂ <= 1 or b₁ <= 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 A2: ( f is being_homeomorphism & f . 0 = p2 & f . 1 = p1 & f . s1 = q2 & 0 <= s1 & s1 <= 1 & f . s2 = q1 & 0 <= s2 & s2 <= 1 ) ; :: thesis: s1 <= s2
then A3: 1 - 0 >= 1 - s1 by XREAL_1:15;
A4: 1 - 0 >= 1 - s2 by A2, XREAL_1:15;
A5: 1 - 1 <= 1 - s1 by A2, XREAL_1:15;
A6: 1 - 1 <= 1 - s2 by A2, XREAL_1:15;
set Ex = L[01] (0 ,1 (#) ),((#) 0 ,1);
A7: L[01] (0 ,1 (#) ),((#) 0 ,1) is being_homeomorphism by TREAL_1:21;
set g = f * (L[01] (0 ,1 (#) ),((#) 0 ,1));
A8: (L[01] (0 ,1 (#) ),((#) 0 ,1)) . (0 ,1 (#) ) = 0 by BORSUK_1:def 17, TREAL_1:8, TREAL_1:12;
A9: (L[01] (0 ,1 (#) ),((#) 0 ,1)) . ((#) 0 ,1) = 1 by BORSUK_1:def 18, TREAL_1:8, TREAL_1:12;
dom f = [#] I[01] by A2, TOPS_2:def 5;
then A10: rng (L[01] (0 ,1 (#) ),((#) 0 ,1)) = dom f by A7, TOPMETR:27, TOPS_2:def 5;
then A11: dom (f * (L[01] (0 ,1 (#) ),((#) 0 ,1))) = dom (L[01] (0 ,1 (#) ),((#) 0 ,1)) by RELAT_1:46;
A12: rng (f * (L[01] (0 ,1 (#) ),((#) 0 ,1))) = rng f by A10, RELAT_1:47;
A13: dom (f * (L[01] (0 ,1 (#) ),((#) 0 ,1))) = [#] I[01] by A7, A11, TOPMETR:27, TOPS_2:def 5;
then reconsider g = f * (L[01] (0 ,1 (#) ),((#) 0 ,1)) as Function of I[01] ,((TOP-REAL 2) | P') by A12, FUNCT_2:def 1, RELSET_1:11;
A14: g is being_homeomorphism by A2, A7, TOPMETR:27, TOPS_2:71;
A15: ( 1 - s1 in dom g & 1 - s2 in dom g ) by A3, A4, A5, A6, A13, BORSUK_1:86;
A16: g . 0 = p1 by A2, A9, A13, BORSUK_1:def 17, FUNCT_1:22, TREAL_1:8;
A17: g . 1 = p2 by A2, A8, A13, BORSUK_1:def 18, FUNCT_1:22, TREAL_1:8;
reconsider qs1 = 1 - s1, qs2 = 1 - s2 as Point of (Closed-Interval-TSpace 0 ,1) by A3, A4, A5, A6, BORSUK_1:86, TOPMETR:27;
A18: (L[01] (0 ,1 (#) ),((#) 0 ,1)) . qs1 = ((1 - (1 - s1)) * 1) + ((1 - s1) * 0 ) by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8, TREAL_1:def 3
.= s1 ;
A19: (L[01] (0 ,1 (#) ),((#) 0 ,1)) . qs2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0 ) by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8, TREAL_1:def 3
.= s2 ;
A20: g . (1 - s1) = q2 by A2, A15, A18, FUNCT_1:22;
g . (1 - s2) = q1 by A2, A15, A19, FUNCT_1:22;
then 1 - s2 <= 1 - s1 by A1, A3, A4, A5, A14, A16, A17, A20, JORDAN5C:def 3;
then s1 <= 1 - (1 - s2) by XREAL_1:13;
hence s1 <= s2 ; :: thesis: verum