let P be non empty compact Subset of (TOP-REAL 2); ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } implies 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 ) )
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 }
; 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 )
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);
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;
( 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.]
;
( r1 < r2 iff q1 `1 < q2 `1 )
A17:
now ( r1 > r2 implies q1 `1 > q2 `1 )
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
;
q1 `1 > q2 `1 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
by SQUARE_1:18
;
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
by SQUARE_1:18
;
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;
verum end;
A34:
now ( q1 `1 < q2 `1 implies r1 < r2 )assume A35:
q1 `1 < q2 `1
;
r1 < r2now not r1 >= r2assume A36:
r1 >= r2
;
contradictionnow ( ( r1 > r2 & contradiction ) or ( r1 = r2 & contradiction ) )end; hence
contradiction
;
verum end; hence
r1 < r2
;
verum end;
now ( r2 > r1 implies q2 `1 > q1 `1 )assume
r2 > r1
;
q2 `1 > q1 `1 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
by SQUARE_1:18
;
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
by SQUARE_1:18
;
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;
verum end;
hence
(
r1 < r2 iff
q1 `1 < q2 `1 )
by A34;
verum
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; verum