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 ) )

proof

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

per cases ( s1 < s2 or s1 = s2 or s1 > s2 ) by XXREAL_0:1;

suppose s1 < s2 ; :: thesis: contradiction

hence contradiction by A1, A16, A5, A6, A9, A11, A12, A15, A13, Th8; :: thesis: verum

end;

suppose s1 = s2 ; :: thesis: contradiction

hence contradiction by A4, A9, A11; :: thesis: verum

end;

suppose s1 > s2 ; :: thesis: contradiction

hence contradiction by A1, A16, A5, A6, A9, A11, A15, A14, A13, Th8; :: thesis: verum

end;

end;

end;

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