let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } implies ex f being Function of I[01],((TOP-REAL 2) | (Lower_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 = E-max P & f . 1 = W-min P ) )
reconsider T = (TOP-REAL 2) | (Lower_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 Th38;
assume A5: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } ; :: thesis: ex f being Function of I[01],((TOP-REAL 2) | (Lower_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 = E-max P & f . 1 = W-min P )
then consider f1 being Function of (Closed-Interval-TSpace ((- 1),1)),((TOP-REAL 2) | (Lower_Arc P)) such that
A6: f1 is being_homeomorphism and
A7: for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
f1 . (q `1) = q and
A8: f1 . (- 1) = W-min P and
A9: f1 . 1 = E-max P by Th40;
reconsider h = f1 * g as Function of I[01],((TOP-REAL 2) | (Lower_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 = E-max P by A9, 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: 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 )
let r1, r2 be Real; :: thesis: ( h . r1 = q1 & h . r2 = q2 & r1 in [.0,1.] & r2 in [.0,1.] implies ( r1 < r2 iff q1 `1 > q2 `1 ) )
assume that
A13: h . r1 = q1 and
A14: h . r2 = q2 and
A15: r1 in [.0,1.] and
A16: r2 in [.0,1.] ; :: thesis: ( r1 < r2 iff q1 `1 > q2 `1 )

A17: now :: thesis: ( r2 < r1 implies q2 `1 > q1 `1 )

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))))]|;
A18: |[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2))))]| `2 = - (sqrt (1 - ((((- 2) * r2) + 1) ^2))) by EUCLID:52;
r2 <= 1 by A16, XXREAL_1:1;
then (- 2) * r2 >= (- 2) * 1 by XREAL_1:65;
then ((- 2) * r2) + 1 >= ((- 2) * 1) + 1 by XREAL_1:7;
then A19: - 1 <= ((- 2) * r2) + 1 ;
r2 >= 0 by A16, XXREAL_1:1;
then ((- 2) * r2) + 1 <= ((- 2) * 0) + 1 by XREAL_1:7;
then (((- 2) * r2) + 1) ^2 <= 1 ^2 by A19, SQUARE_1:49;
then A20: 1 - ((((- 2) * r2) + 1) ^2) >= 0 by XREAL_1:48;
then A21: sqrt (1 - ((((- 2) * r2) + 1) ^2)) >= 0 by SQUARE_1:def 2;
|.|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2))))]|.| = sqrt (((|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2))))]| `1) ^2) + ((|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2))))]| `2) ^2)) by JGRAPH_3:1
.= sqrt (((((- 2) * r2) + 1) ^2) + ((sqrt (1 - ((((- 2) * r2) + 1) ^2))) ^2)) by A18, EUCLID:52
.= sqrt (((((- 2) * r2) + 1) ^2) + (1 - ((((- 2) * r2) + 1) ^2))) by A20, 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 A18, A21;
then A22: ( |[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2))))]| `1 = ((- 2) * r2) + 1 & |[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2))))]| in Lower_Arc P ) by A5, Th35, EUCLID:52;
( 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, A22 ;
then A23: q2 `1 = ((- 2) * r2) + 1 by A14, EUCLID:52;
A24: |[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2))))]| `1 = ((- 2) * r1) + 1 by EUCLID:52;
r1 <= 1 by A15, XXREAL_1:1;
then (- 2) * r1 >= (- 2) * 1 by XREAL_1:65;
then ((- 2) * r1) + 1 >= ((- 2) * 1) + 1 by XREAL_1:7;
then A25: - 1 <= ((- 2) * r1) + 1 ;
r1 >= 0 by A15, XXREAL_1:1;
then ((- 2) * r1) + 1 <= ((- 2) * 0) + 1 by XREAL_1:7;
then (((- 2) * r1) + 1) ^2 <= 1 ^2 by A25, 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;
assume r2 < r1 ; :: thesis: q2 `1 > q1 `1
then A28: (- 2) * r2 > (- 2) * r1 by XREAL_1:69;
A29: |[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2))))]| `2 = - (sqrt (1 - ((((- 2) * r1) + 1) ^2))) by EUCLID:52;
|.|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2))))]|.| = sqrt (((|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2))))]| `1) ^2) + ((|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2))))]| `2) ^2)) by JGRAPH_3:1
.= sqrt (((((- 2) * r1) + 1) ^2) + ((sqrt (1 - ((((- 2) * r1) + 1) ^2))) ^2)) by A29, EUCLID:52
.= 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 A29, A27;
then A30: |[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2))))]| in Lower_Arc P by A5, Th35;
( 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, A24, A30 ;
hence q2 `1 > q1 `1 by A13, A28, A23, A24, XREAL_1:8; :: thesis: verum

end;

A31: now :: thesis: ( q1 `1 > q2 `1 implies r1 < r2 )

assume A32: q1 `1 > q2 `1 ; :: thesis: r1 < r2

now :: thesis: not r1 >= r2

assume A33: r1 >= r2 ; :: thesis: contradiction

now :: thesis: ( ( r1 > r2 & contradiction ) or ( r1 = r2 & contradiction ) )

per cases ( r1 > r2 or r1 = r2 ) by A33, XXREAL_0:1;

case r1 > r2 ; :: thesis: contradiction

hence contradiction by A17, A32; :: thesis: verum

end;

case r1 = r2 ; :: thesis: contradiction

hence contradiction by A13, A14, A32; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence r1 < r2 ; :: thesis: verum

end;

now :: thesis: ( r1 < r2 implies q1 `1 > q2 `1 )

assume r1 < r2 ; :: thesis: q1 `1 > q2 `1
then (- 2) * r1 > (- 2) * r2 by XREAL_1:69;
then A34: ((- 2) * r1) + 1 > ((- 2) * r2) + 1 by XREAL_1:8;
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))))]|;
A35: |[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2))))]| `2 = - (sqrt (1 - ((((- 2) * r1) + 1) ^2))) by EUCLID:52;
r1 <= 1 by A15, XXREAL_1:1;
then (- 2) * r1 >= (- 2) * 1 by XREAL_1:65;
then ((- 2) * r1) + 1 >= ((- 2) * 1) + 1 by XREAL_1:7;
then A36: - 1 <= ((- 2) * r1) + 1 ;
r1 >= 0 by A15, XXREAL_1:1;
then ((- 2) * r1) + 1 <= ((- 2) * 0) + 1 by XREAL_1:7;
then (((- 2) * r1) + 1) ^2 <= 1 ^2 by A36, SQUARE_1:49;
then A37: 1 - ((((- 2) * r1) + 1) ^2) >= 0 by XREAL_1:48;
then A38: sqrt (1 - ((((- 2) * r1) + 1) ^2)) >= 0 by SQUARE_1:def 2;
|.|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2))))]|.| = sqrt (((|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2))))]| `1) ^2) + ((|[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2))))]| `2) ^2)) by JGRAPH_3:1
.= sqrt (((((- 2) * r1) + 1) ^2) + ((sqrt (1 - ((((- 2) * r1) + 1) ^2))) ^2)) by A35, EUCLID:52
.= sqrt (((((- 2) * r1) + 1) ^2) + (1 - ((((- 2) * r1) + 1) ^2))) by A37, 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 A35, A38;
then A39: ( |[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2))))]| `1 = ((- 2) * r1) + 1 & |[(((- 2) * r1) + 1),(- (sqrt (1 - ((((- 2) * r1) + 1) ^2))))]| in Lower_Arc P ) by A5, Th35, EUCLID:52;
( 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, A39 ;
then A40: q1 `1 = ((- 2) * r1) + 1 by A13, EUCLID:52;
A41: |[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2))))]| `2 = - (sqrt (1 - ((((- 2) * r2) + 1) ^2))) by EUCLID:52;
r2 <= 1 by A16, XXREAL_1:1;
then (- 2) * r2 >= (- 2) * 1 by XREAL_1:65;
then ((- 2) * r2) + 1 >= ((- 2) * 1) + 1 by XREAL_1:7;
then A42: - 1 <= ((- 2) * r2) + 1 ;
r2 >= 0 by A16, XXREAL_1:1;
then ((- 2) * r2) + 1 <= ((- 2) * 0) + 1 by XREAL_1:7;
then (((- 2) * r2) + 1) ^2 <= 1 ^2 by A42, SQUARE_1:49;
then A43: 1 - ((((- 2) * r2) + 1) ^2) >= 0 by XREAL_1:48;
then A44: sqrt (1 - ((((- 2) * r2) + 1) ^2)) >= 0 by SQUARE_1:def 2;
|.|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2))))]|.| = sqrt (((|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2))))]| `1) ^2) + ((|[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2))))]| `2) ^2)) by JGRAPH_3:1
.= sqrt (((((- 2) * r2) + 1) ^2) + ((sqrt (1 - ((((- 2) * r2) + 1) ^2))) ^2)) by A41, EUCLID:52
.= sqrt (((((- 2) * r2) + 1) ^2) + (1 - ((((- 2) * r2) + 1) ^2))) by A43, 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 A41, A44;
then A45: ( |[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2))))]| `1 = ((- 2) * r2) + 1 & |[(((- 2) * r2) + 1),(- (sqrt (1 - ((((- 2) * r2) + 1) ^2))))]| in Lower_Arc P ) by A5, Th35, EUCLID:52;
( 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, A45 ;
hence q1 `1 > q2 `1 by A14, A34, A40, EUCLID:52; :: thesis: verum

end;

hence ( r1 < r2 iff q1 `1 > q2 `1 ) by A31; :: thesis: verum

end;

1 in dom h by A10, XXREAL_1:1;
then A46: h . 1 = W-min P by A8, 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) | (Lower_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 = E-max P & f . 1 = W-min P ) by A12, A11, A46; :: thesis: verum