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₁ being Element of K16(K17( the carrier of I[01], the carrier of ((TOP-REAL 2) | P)))
for b₂, b₃ being object 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 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₁, b₂ being object 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 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