let P be Subset of (); :: thesis: for p1, p2, q1, q2 being Point of () 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 (); :: 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 b1 being Element of K16(K17( the carrier of I, the carrier of (() | P)))
for b2, b3 being object holds
( not b1 is being_homeomorphism or not b1 . 0 = p2 or not b1 . 1 = p1 or not b1 . b2 = q2 or not 0 <= b2 or not b2 <= 1 or not b1 . b3 = q1 or not 0 <= b3 or not b3 <= 1 or b2 <= b3 )

reconsider P9 = P as non empty Subset of () by ;
let f be Function of I,(() | P); :: thesis: for b1, b2 being object holds
( not f is being_homeomorphism or not f . 0 = p2 or not f . 1 = p1 or not f . b1 = q2 or not 0 <= b1 or not b1 <= 1 or not f . b2 = q1 or not 0 <= b2 or not b2 <= 1 or b1 <= b2 )

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 ;
A13: 1 - 0 >= 1 - s2 by ;
A14: 1 - 1 <= 1 - s1 by ;
A15: 1 - 1 <= 1 - s2 by ;
set Ex = L (((0,1) (#)),((#) (0,1)));
A16: L (((0,1) (#)),((#) (0,1))) is being_homeomorphism by TREAL_1:18;
set g = f * (L (((0,1) (#)),((#) (0,1))));
A17: (L (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) = 0 by ;
A18: (L (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) = 1 by ;
dom f = [#] I by ;
then rng (L (((0,1) (#)),((#) (0,1)))) = dom f by ;
then dom (f * (L (((0,1) (#)),((#) (0,1))))) = dom (L (((0,1) (#)),((#) (0,1)))) by RELAT_1:27;
then A19: dom (f * (L (((0,1) (#)),((#) (0,1))))) = [#] I by ;
reconsider g = f * (L (((0,1) (#)),((#) (0,1)))) as Function of I,(() | P9) by TOPMETR:20;
A20: g is being_homeomorphism by ;
A21: 1 - s1 in dom g by ;
A22: 1 - s2 in dom g by ;
A23: g . 0 = p1 by ;
A24: g . 1 = p2 by ;
reconsider qs1 = 1 - s1, qs2 = 1 - s2 as Point of () by ;
A25: (L (((0,1) (#)),((#) (0,1)))) . qs1 = ((1 - (1 - s1)) * 1) + ((1 - s1) * 0) by
.= s1 ;
A26: (L (((0,1) (#)),((#) (0,1)))) . qs2 = ((1 - (1 - s2)) * 1) + ((1 - s2) * 0) by
.= s2 ;
A27: g . (1 - s1) = q2 by ;
g . (1 - s2) = q1 by ;
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