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 & q1 in P & q2 in P & q1 <> q2 & not ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) holds

( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 )

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

assume that

A1: P is_an_arc_of p1,p2 and

A2: q1 in P and

A3: q2 in P and

A4: q1 <> q2 ; :: thesis: ( ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) or ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) )

reconsider P = P as non empty Subset of (TOP-REAL 2) by A2;

( ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) or ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) )

( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 )

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

assume that

A1: P is_an_arc_of p1,p2 and

A2: q1 in P and

A3: q2 in P and

A4: q1 <> q2 ; :: thesis: ( ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) or ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) )

reconsider P = P as non empty Subset of (TOP-REAL 2) by A2;

( ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) or ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) )

proof

hence
( ( LE q1,q2,P,p1,p2 & not LE q2,q1,P,p1,p2 ) or ( LE q2,q1,P,p1,p2 & not LE q1,q2,P,p1,p2 ) )
; :: thesis: verum
consider f being Function of I[01],((TOP-REAL 2) | P) such that

A5: f is being_homeomorphism and

A6: ( f . 0 = p1 & f . 1 = p2 ) by A1, TOPREAL1:def 1;

A7: rng f = [#] ((TOP-REAL 2) | P) by A5, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

then consider x being object such that

A8: x in dom f and

A9: q1 = f . x by A2, FUNCT_1:def 3;

consider y being object such that

A10: y in dom f and

A11: q2 = f . y by A3, A7, FUNCT_1:def 3;

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

.= [.0,1.] by BORSUK_1:40 ;

then reconsider s1 = x, s2 = y as Real by A8, A10;

A12: 0 <= s1 by A8, BORSUK_1:43;

A13: s2 <= 1 by A10, BORSUK_1:43;

A14: 0 <= s2 by A10, BORSUK_1:43;

A15: s1 <= 1 by A8, BORSUK_1:43;

assume A16: ( LE q1,q2,P,p1,p2 iff LE q2,q1,P,p1,p2 ) ; :: thesis: contradiction

end;A5: f is being_homeomorphism and

A6: ( f . 0 = p1 & f . 1 = p2 ) by A1, TOPREAL1:def 1;

A7: rng f = [#] ((TOP-REAL 2) | P) by A5, TOPS_2:def 5

.= P by PRE_TOPC:def 5 ;

then consider x being object such that

A8: x in dom f and

A9: q1 = f . x by A2, FUNCT_1:def 3;

consider y being object such that

A10: y in dom f and

A11: q2 = f . y by A3, A7, FUNCT_1:def 3;

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

.= [.0,1.] by BORSUK_1:40 ;

then reconsider s1 = x, s2 = y as Real by A8, A10;

A12: 0 <= s1 by A8, BORSUK_1:43;

A13: s2 <= 1 by A10, BORSUK_1:43;

A14: 0 <= s2 by A10, BORSUK_1:43;

A15: s1 <= 1 by A8, BORSUK_1:43;

assume A16: ( LE q1,q2,P,p1,p2 iff LE q2,q1,P,p1,p2 ) ; :: thesis: contradiction