let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
reconsider T = (TOP-REAL 2) | (Upper_Arc P) as non empty TopSpace ;
consider g being Function of I[01],(Closed-Interval-TSpace ((- 1),1)) such that
A1: g is being_homeomorphism and
A2: for r being Real st r in [.0,1.] holds
g . r = (2 * r) - 1 and
A3: g . 0 = - 1 and
A4: g . 1 = 1 by Th39;
assume A5: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } ; :: thesis:
then consider f1 being Function of (Closed-Interval-TSpace ((- 1),1)),((TOP-REAL 2) | (Upper_Arc P)) such that
A6: f1 is being_homeomorphism and
A7: for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds
f1 . (q `1) = q and
A8: f1 . (- 1) = W-min P and
A9: f1 . 1 = E-max P by Th41;
reconsider h = f1 * g as Function of I[01],((TOP-REAL 2) | (Upper_Arc P)) ;
A10: dom h = [.0,1.] by BORSUK_1:40, FUNCT_2:def 1;
then 0 in dom h by XXREAL_1:1;
then A11: h . 0 = W-min P by A8, A3, FUNCT_1:12;
A12: for q1, q2 being Point of (TOP-REAL 2)
for r1, r2 being Real st h . r1 = q1 & h . r2 = q2 & r1 in [.0,1.] & r2 in [.0,1.] holds
( r1 < r2 iff q1 `1 < q2 `1 )

proof

let q1, q2 be Point of (TOP-REAL 2); :: thesis:
let r1, r2 be Real; :: thesis:
assume that
A13: h . r1 = q1 and
A14: h . r2 = q2 and
A15: r1 in [.0,1.] and
A16: r2 in [.0,1.] ; :: thesis:

A17: now :: thesis:

r2 <= 1 by A16, XXREAL_1:1;
then 2 * r2 <= 2 * 1 by XREAL_1:64;
then A18: (2 * r2) - 1 <= (2 * 1) - 1 by XREAL_1:9;
r1 >= 0 by A15, XXREAL_1:1;
then A19: (2 * r1) - 1 >= (2 * 0) - 1 by XREAL_1:9;
set s1 = (2 * r1) - 1;
set s2 = (2 * r2) - 1;
set p1 = |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]|;
set p2 = |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]|;
A20: |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]| `1 = (2 * r1) - 1 by EUCLID:52;
r2 >= 0 by A16, XXREAL_1:1;
then A21: (2 * r2) - 1 >= (2 * 0) - 1 by XREAL_1:9;
(2 * 0) - 1 = - 1 ;
then ((2 * r2) - 1) ^2 <= 1 ^2 by A18, A21, SQUARE_1:49;
then A22: 1 - (((2 * r2) - 1) ^2) >= 0 by XREAL_1:48;
then A23: sqrt (1 - (((2 * r2) - 1) ^2)) >= 0 by SQUARE_1:def 2;
r1 <= 1 by A15, XXREAL_1:1;
then 2 * r1 <= 2 * 1 by XREAL_1:64;
then A24: (2 * r1) - 1 <= (2 * 1) - 1 by XREAL_1:9;
assume r1 > r2 ; :: thesis:
then A25: 2 * r1 > 2 * r2 by XREAL_1:68;
(2 * 0) - 1 = - 1 ;
then ((2 * r1) - 1) ^2 <= 1 ^2 by A24, A19, SQUARE_1:49;
then A26: 1 - (((2 * r1) - 1) ^2) >= 0 by XREAL_1:48;
then A27: sqrt (1 - (((2 * r1) - 1) ^2)) >= 0 by SQUARE_1:def 2;
A28: |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]| `2 = sqrt (1 - (((2 * r1) - 1) ^2)) by EUCLID:52;
then |.|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]|.| = sqrt ((((2 * r1) - 1) ^2) + ((sqrt (1 - (((2 * r1) - 1) ^2))) ^2)) by A20, JGRAPH_3:1
.= sqrt ((((2 * r1) - 1) ^2) + (1 - (((2 * r1) - 1) ^2))) by A26, SQUARE_1:def 2
.= 1 ;
then |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]| in P by A5;
then |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]| in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) } by A28, A27;
then A29: |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]| in Upper_Arc P by A5, Th34;
( g . r1 = (2 * r1) - 1 & dom h = [.0,1.] ) by A2, A15, BORSUK_1:40, FUNCT_2:def 1;
then h . r1 = f1 . ((2 * r1) - 1) by A15, FUNCT_1:12
.= |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]| by A7, A20, A29 ;
then A30: q1 `1 = (2 * r1) - 1 by A13, EUCLID:52;
A31: |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]| `1 = (2 * r2) - 1 by EUCLID:52;
A32: |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]| `2 = sqrt (1 - (((2 * r2) - 1) ^2)) by EUCLID:52;
then |.|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]|.| = sqrt ((((2 * r2) - 1) ^2) + ((sqrt (1 - (((2 * r2) - 1) ^2))) ^2)) by A31, JGRAPH_3:1
.= sqrt ((((2 * r2) - 1) ^2) + (1 - (((2 * r2) - 1) ^2))) by A22, SQUARE_1:def 2
.= 1 ;
then |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]| in P by A5;
then |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]| in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) } by A32, A23;
then A33: |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]| in Upper_Arc P by A5, Th34;
( g . r2 = (2 * r2) - 1 & dom h = [.0,1.] ) by A2, A16, BORSUK_1:40, FUNCT_2:def 1;
then h . r2 = f1 . ((2 * r2) - 1) by A16, FUNCT_1:12
.= |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]| by A7, A31, A33 ;
hence q1 `1 > q2 `1 by A14, A25, A30, A31, XREAL_1:14; :: thesis:

end;

A34: now :: thesis:

assume A35: q1 `1 < q2 `1 ; :: thesis:

now :: thesis:

assume A36: r1 >= r2 ; :: thesis:

now :: thesis:

per cases by A36, XXREAL_0:1;

case r1 > r2 ; :: thesis:

hence contradiction by A17, A35; :: thesis:

end;

case r1 = r2 ; :: thesis:

hence contradiction by A13, A14, A35; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence r1 < r2 ; :: thesis:

end;

now :: thesis:

assume r2 > r1 ; :: thesis:
then A37: 2 * r2 > 2 * r1 by XREAL_1:68;
set s1 = (2 * r2) - 1;
set s2 = (2 * r1) - 1;
set p1 = |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]|;
set p2 = |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]|;
A38: |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]| `1 = (2 * r2) - 1 by EUCLID:52;
r2 >= 0 by A16, XXREAL_1:1;
then (2 * r2) - 1 >= (2 * 0) - 1 by XREAL_1:9;
then A39: - 1 <= (2 * r2) - 1 ;
r2 <= 1 by A16, XXREAL_1:1;
then 2 * r2 <= 2 * 1 by XREAL_1:64;
then (2 * r2) - 1 <= (2 * 1) - 1 by XREAL_1:9;
then ((2 * r2) - 1) ^2 <= 1 ^2 by A39, SQUARE_1:49;
then A40: 1 - (((2 * r2) - 1) ^2) >= 0 by XREAL_1:48;
then A41: sqrt (1 - (((2 * r2) - 1) ^2)) >= 0 by SQUARE_1:def 2;
A42: |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]| `2 = sqrt (1 - (((2 * r2) - 1) ^2)) by EUCLID:52;
then |.|[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]|.| = sqrt ((((2 * r2) - 1) ^2) + ((sqrt (1 - (((2 * r2) - 1) ^2))) ^2)) by A38, JGRAPH_3:1
.= sqrt ((((2 * r2) - 1) ^2) + (1 - (((2 * r2) - 1) ^2))) by A40, SQUARE_1:def 2
.= 1 ;
then |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]| in P by A5;
then |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]| in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) } by A42, A41;
then A43: |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]| in Upper_Arc P by A5, Th34;
( g . r2 = (2 * r2) - 1 & dom h = [.0,1.] ) by A2, A16, BORSUK_1:40, FUNCT_2:def 1;
then h . r2 = f1 . ((2 * r2) - 1) by A16, FUNCT_1:12
.= |[((2 * r2) - 1),(sqrt (1 - (((2 * r2) - 1) ^2)))]| by A7, A38, A43 ;
then A44: q2 `1 = (2 * r2) - 1 by A14, EUCLID:52;
A45: |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]| `1 = (2 * r1) - 1 by EUCLID:52;
r1 >= 0 by A15, XXREAL_1:1;
then (2 * r1) - 1 >= (2 * 0) - 1 by XREAL_1:9;
then A46: - 1 <= (2 * r1) - 1 ;
r1 <= 1 by A15, XXREAL_1:1;
then 2 * r1 <= 2 * 1 by XREAL_1:64;
then (2 * r1) - 1 <= (2 * 1) - 1 by XREAL_1:9;
then ((2 * r1) - 1) ^2 <= 1 ^2 by A46, SQUARE_1:49;
then A47: 1 - (((2 * r1) - 1) ^2) >= 0 by XREAL_1:48;
then A48: sqrt (1 - (((2 * r1) - 1) ^2)) >= 0 by SQUARE_1:def 2;
A49: |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]| `2 = sqrt (1 - (((2 * r1) - 1) ^2)) by EUCLID:52;
then |.|[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]|.| = sqrt ((((2 * r1) - 1) ^2) + ((sqrt (1 - (((2 * r1) - 1) ^2))) ^2)) by A45, JGRAPH_3:1
.= sqrt ((((2 * r1) - 1) ^2) + (1 - (((2 * r1) - 1) ^2))) by A47, SQUARE_1:def 2
.= 1 ;
then |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]| in P by A5;
then |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]| in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) } by A49, A48;
then A50: |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]| in Upper_Arc P by A5, Th34;
( g . r1 = (2 * r1) - 1 & dom h = [.0,1.] ) by A2, A15, BORSUK_1:40, FUNCT_2:def 1;
then h . r1 = f1 . ((2 * r1) - 1) by A15, FUNCT_1:12
.= |[((2 * r1) - 1),(sqrt (1 - (((2 * r1) - 1) ^2)))]| by A7, A45, A50 ;
hence q2 `1 > q1 `1 by A13, A37, A44, A45, XREAL_1:14; :: thesis:

end;

hence ( r1 < r2 iff q1 `1 < q2 `1 ) by A34; :: thesis:

end;

1 in dom h by A10, XXREAL_1:1;
then A51: h . 1 = E-max P by A9, A4, FUNCT_1:12;
reconsider f2 = f1 as Function of (Closed-Interval-TSpace ((- 1),1)),T ;
f2 * g is being_homeomorphism by A6, A1, TOPS_2:57;
hence ex f being Function of I[01],((TOP-REAL 2) | (Upper_Arc P)) st
( f is being_homeomorphism & ( for q1, q2 being Point of (TOP-REAL 2)
for r1, r2 being Real st f . r1 = q1 & f . r2 = q2 & r1 in [.0,1.] & r2 in [.0,1.] holds
( r1 < r2 iff q1 `1 < q2 `1 ) ) & f . 0 = W-min P & f . 1 = E-max P ) by A12, A11, A51; :: thesis: