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 A1: ( P is_an_arc_of p1,p2 & q1 in P & q2 in P & 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 ) )
then reconsider P = P as non empty Subset of (TOP-REAL 2) ;
( ( 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

assume A2: ( LE q1,q2,P,p1,p2 iff LE q2,q1,P,p1,p2 ) ; :: thesis: contradiction
consider f being Function of I[01] ,((TOP-REAL 2) | P) such that
A3: ( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) by A1, TOPREAL1:def 2;
A4: rng f = [#] ((TOP-REAL 2) | P) by A3, TOPS_2:def 5
.= P by PRE_TOPC:def 10 ;
then consider x being set such that
A5: ( x in dom f & q1 = f . x ) by A1, FUNCT_1:def 5;
consider y being set such that
A6: ( y in dom f & q2 = f . y ) by A1, A4, FUNCT_1:def 5;
dom f = [#] I[01] by A3, TOPS_2:def 5
.= [.0 ,1.] by BORSUK_1:83 ;
then reconsider s1 = x, s2 = y as Real by A5, A6;
A7: ( f . s1 = q1 & 0 <= s1 & s1 <= 1 & f . s2 = q2 & 0 <= s2 & s2 <= 1 ) by A5, A6, BORSUK_1:86;

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

suppose s1 < s2 ; :: thesis: contradiction

hence contradiction by A1, A2, A3, A7, Th8, Th12; :: thesis: verum

end;

suppose s1 = s2 ; :: thesis: contradiction

hence contradiction by A1, A5, A6; :: thesis: verum

end;

suppose s1 > s2 ; :: thesis: contradiction

hence contradiction by A1, A2, A3, A7, Th8, Th12; :: 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