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 & 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); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

q1 = q2

let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum