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 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 holds
q1 = q2
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ( P is_an_arc_of p1,p2 & LE q1,q2,P,p1,p2 & LE q2,q1,P,p1,p2 implies q1 = q2 )
assume that
A1:
P is_an_arc_of p1,p2
and
A2:
LE q1,q2,P,p1,p2
and
A3:
LE q2,q1,P,p1,p2
; q1 = q2
consider f being Function of I[01],((TOP-REAL 2) | P) such that
A4:
f is being_homeomorphism
and
A5:
( f . 0 = p1 & f . 1 = p2 )
by A1, TOPREAL1:def 1;
A6: dom f =
[#] I[01]
by A4, TOPS_2:def 5
.=
the carrier of I[01]
;
A7: rng f =
[#] ((TOP-REAL 2) | P)
by A4, TOPS_2:def 5
.=
P
by PRE_TOPC:def 5
;
then
q2 in rng f
by A2;
then consider x being object such that
A8:
x in dom f
and
A9:
q2 = f . x
by FUNCT_1:def 3;
q1 in rng f
by A2, A7;
then consider y being object such that
A10:
y in dom f
and
A11:
q1 = f . y
by FUNCT_1:def 3;
[.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) }
by RCOMP_1:def 1;
then consider s3 being Real such that
A12:
s3 = x
and
A13:
( 0 <= s3 & s3 <= 1 )
by A6, A8, BORSUK_1:40;
[.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) }
by RCOMP_1:def 1;
then consider s4 being Real such that
A14:
s4 = y
and
A15:
( 0 <= s4 & s4 <= 1 )
by A6, A10, BORSUK_1:40;
( s3 <= s4 & s4 <= s3 )
by A2, A3, A4, A5, A9, A12, A13, A11, A14, A15;
hence
q1 = q2
by A9, A12, A11, A14, XXREAL_0:1; verum