let P be Subset of (TOP-REAL 2); 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); ( 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
; ( ( 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 2;
A7:
rng f =
[#] ((TOP-REAL 2) | P)
by A5, TOPS_2:def 5
.=
P
by PRE_TOPC:def 10
;
then consider x being
set such that A8:
x in dom f
and A9:
q1 = f . x
by A2, FUNCT_1:def 5;
consider y being
set such that A10:
y in dom f
and A11:
q2 = f . y
by A3, A7, FUNCT_1:def 5;
dom f =
[#] I[01]
by A5, TOPS_2:def 5
.=
[.0 ,1.]
by BORSUK_1:83
;
then reconsider s1 =
x,
s2 =
y as
Real by A8, A10;
A12:
0 <= s1
by A8, BORSUK_1:86;
A13:
s2 <= 1
by A10, BORSUK_1:86;
A14:
0 <= s2
by A10, BORSUK_1:86;
A15:
s1 <= 1
by A8, BORSUK_1:86;
assume A16:
(
LE q1,
q2,
P,
p1,
p2 iff
LE q2,
q1,
P,
p1,
p2 )
;
contradiction
per cases
( s1 < s2 or s1 = s2 or s1 > s2 )
by XXREAL_0:1;
suppose
s1 < s2
;
contradictionhence
contradiction
by A1, A4, A16, A5, A6, A9, A11, A12, A15, A13, Th8, Th12;
verum end; suppose
s1 = s2
;
contradictionhence
contradiction
by A4, A9, A11;
verum end; suppose
s1 > s2
;
contradictionhence
contradiction
by A1, A4, A16, A5, A6, A9, A11, A15, A14, A13, Th8, Th12;
verum 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 ) )
; verum