let p1, p2, p3, p4 be Point of (TOP-REAL 2); for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1 `1 < 0 & p1 `2 >= 0 & p2 `1 < 0 & p2 `2 >= 0 & p3 `1 < 0 & p3 `2 >= 0 & p4 `1 < 0 & p4 `2 >= 0 holds
ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
let P be non empty compact Subset of (TOP-REAL 2); ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & p1 `1 < 0 & p1 `2 >= 0 & p2 `1 < 0 & p2 `2 >= 0 & p3 `1 < 0 & p3 `2 >= 0 & p4 `1 < 0 & p4 `2 >= 0 implies ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) )
assume that
A1:
P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 }
and
A2:
LE p1,p2,P
and
A3:
LE p2,p3,P
and
A4:
LE p3,p4,P
and
A5:
p1 `1 < 0
and
A6:
p1 `2 >= 0
and
A7:
p2 `1 < 0
and
A8:
p2 `2 >= 0
and
A9:
p3 `1 < 0
and
A10:
p3 `2 >= 0
and
A11:
p4 `1 < 0
and
A12:
p4 `2 >= 0
; ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
consider r being Real such that
A13:
p4 `1 < r
and
A14:
r < 0
by A11, XREAL_1:5;
reconsider r1 = r as Real ;
set s = sqrt (1 - (r1 ^2));
A15:
P is being_simple_closed_curve
by A1, JGRAPH_3:26;
then
p4 in P
by A4, JORDAN7:5;
then A16:
ex p being Point of (TOP-REAL 2) st
( p = p4 & |.p.| = 1 )
by A1;
then
- 1 <= p4 `1
by Th1;
then
- 1 <= r1
by A13, XXREAL_0:2;
then
r1 ^2 <= 1 ^2
by A14, SQUARE_1:49;
then A17:
1 - (r1 ^2) >= 0
by XREAL_1:48;
then A18:
(sqrt (1 - (r1 ^2))) ^2 = 1 - (r1 ^2)
by SQUARE_1:def 2;
then A19:
(1 - ((sqrt (1 - (r1 ^2))) ^2)) + ((sqrt (1 - (r1 ^2))) ^2) > 0 + ((sqrt (1 - (r1 ^2))) ^2)
by A14, SQUARE_1:12, XREAL_1:8;
then A20:
- 1 < sqrt (1 - (r1 ^2))
by SQUARE_1:52;
A21:
sqrt (1 - (r1 ^2)) < 1
by A19, SQUARE_1:52;
then consider f1 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A22:
f1 = (sqrt (1 - (r1 ^2))) -FanMorphW
and
A23:
f1 is being_homeomorphism
by A20, JGRAPH_4:41;
set q11 = f1 . p1;
set q22 = f1 . p2;
set q33 = f1 . p3;
set q44 = f1 . p4;
A24:
sqrt (1 - (r1 ^2)) >= 0
by A17, SQUARE_1:def 2;
p3 in P
by A3, A15, JORDAN7:5;
then A25:
ex p33 being Point of (TOP-REAL 2) st
( p33 = p3 & |.p33.| = 1 )
by A1;
then
( (p3 `2) / |.p3.| < (p4 `2) / |.p4.| or p3 = p4 )
by A1, A4, A11, A12, A16, Th46;
then A26:
( ((f1 . p3) `2) / |.(f1 . p3).| < ((f1 . p4) `2) / |.(f1 . p4).| or p3 = p4 )
by A9, A11, A20, A21, A22, JGRAPH_4:46;
(p4 `1) ^2 > r1 ^2
by A13, A14, SQUARE_1:44;
then A27:
1 - ((p4 `1) ^2) < 1 - (r1 ^2)
by XREAL_1:15;
A28:
( p3 `1 < p4 `1 or p3 = p4 )
by A1, A4, A9, A10, A12, Th46;
then
- (p3 `1) >= - (p4 `1)
by XREAL_1:24;
then
(- (p3 `1)) ^2 >= (- (p4 `1)) ^2
by A11, SQUARE_1:15;
then
1 - ((p3 `1) ^2) <= 1 - ((p4 `1) ^2)
by XREAL_1:10;
then A29:
1 - ((p3 `1) ^2) < (sqrt (1 - (r1 ^2))) ^2
by A27, A18, XXREAL_0:2;
( p2 `1 < p3 `1 or p2 = p3 )
by A1, A3, A7, A8, A10, Th46;
then A30:
p2 `1 <= p4 `1
by A28, XXREAL_0:2;
then
- (p2 `1) >= - (p4 `1)
by XREAL_1:24;
then
(- (p2 `1)) ^2 >= (- (p4 `1)) ^2
by A11, SQUARE_1:15;
then
1 - ((p2 `1) ^2) <= 1 - ((p4 `1) ^2)
by XREAL_1:10;
then A31:
1 - ((p2 `1) ^2) < (sqrt (1 - (r1 ^2))) ^2
by A27, A18, XXREAL_0:2;
( p1 `1 < p2 `1 or p1 = p2 )
by A1, A2, A5, A6, A8, Th46;
then
p1 `1 <= p4 `1
by A30, XXREAL_0:2;
then
- (p1 `1) >= - (p4 `1)
by XREAL_1:24;
then
(- (p1 `1)) ^2 >= (- (p4 `1)) ^2
by A11, SQUARE_1:15;
then
1 - ((p1 `1) ^2) <= 1 - ((p4 `1) ^2)
by XREAL_1:10;
then A32:
1 - ((p1 `1) ^2) < (sqrt (1 - (r1 ^2))) ^2
by A27, A18, XXREAL_0:2;
1 ^2 = ((p3 `1) ^2) + ((p3 `2) ^2)
by A25, JGRAPH_3:1;
then A33:
(p3 `2) / |.p3.| < sqrt (1 - (r1 ^2))
by A25, A24, A29, SQUARE_1:48;
then A34:
(f1 . p3) `1 < 0
by A9, A20, A22, JGRAPH_4:43;
p2 in P
by A2, A15, JORDAN7:5;
then A35:
ex p22 being Point of (TOP-REAL 2) st
( p22 = p2 & |.p22.| = 1 )
by A1;
then A36:
|.(f1 . p2).| = 1
by A22, JGRAPH_4:33;
then A37:
f1 . p2 in P
by A1;
( (p2 `2) / |.p2.| < (p3 `2) / |.p3.| or p2 = p3 )
by A1, A3, A9, A10, A35, A25, Th46;
then A38:
( ((f1 . p2) `2) / |.(f1 . p2).| < ((f1 . p3) `2) / |.(f1 . p3).| or p2 = p3 )
by A7, A9, A20, A21, A22, JGRAPH_4:46;
A39:
|.(f1 . p3).| = 1
by A25, A22, JGRAPH_4:33;
then A40:
f1 . p3 in P
by A1;
1 ^2 = ((p2 `1) ^2) + ((p2 `2) ^2)
by A35, JGRAPH_3:1;
then A41:
(p2 `2) / |.p2.| < sqrt (1 - (r1 ^2))
by A35, A24, A31, SQUARE_1:48;
then A42:
(f1 . p2) `2 < 0
by A7, A20, A22, JGRAPH_4:43;
A43:
(f1 . p2) `1 < 0
by A7, A20, A22, A41, JGRAPH_4:43;
1 ^2 = ((p4 `1) ^2) + ((p4 `2) ^2)
by A16, JGRAPH_3:1;
then
(p4 `2) / |.p4.| < sqrt (1 - (r1 ^2))
by A27, A16, A18, A24, SQUARE_1:48;
then A44:
( (f1 . p4) `1 < 0 & (f1 . p4) `2 < 0 )
by A11, A20, A22, JGRAPH_4:43;
p1 in P
by A2, A15, JORDAN7:5;
then A45:
ex p11 being Point of (TOP-REAL 2) st
( p11 = p1 & |.p11.| = 1 )
by A1;
then
( (p1 `2) / |.p1.| < (p2 `2) / |.p2.| or p1 = p2 )
by A1, A2, A7, A8, A35, Th46;
then A46:
( ((f1 . p1) `2) / |.(f1 . p1).| < ((f1 . p2) `2) / |.(f1 . p2).| or p1 = p2 )
by A5, A7, A20, A21, A22, JGRAPH_4:46;
1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2)
by A45, JGRAPH_3:1;
then A47:
(p1 `2) / |.p1.| < sqrt (1 - (r1 ^2))
by A45, A24, A32, SQUARE_1:48;
then A48:
(f1 . p1) `1 < 0
by A5, A20, A22, JGRAPH_4:43;
A49:
|.(f1 . p1).| = 1
by A45, A22, JGRAPH_4:33;
then
f1 . p1 in P
by A1;
then A50:
LE f1 . p1,f1 . p2,P
by A1, A49, A36, A37, A48, A43, A42, A46, Th51;
A51:
( (f1 . p2) `1 < 0 & (f1 . p2) `2 < 0 )
by A7, A20, A22, A41, JGRAPH_4:43;
A52:
( (f1 . p1) `1 < 0 & (f1 . p1) `2 < 0 )
by A5, A20, A22, A47, JGRAPH_4:43;
A53:
for q being Point of (TOP-REAL 2) holds |.(f1 . q).| = |.q.|
by A22, JGRAPH_4:33;
( (f1 . p3) `1 < 0 & (f1 . p3) `2 < 0 )
by A9, A20, A22, A33, JGRAPH_4:43;
then A54:
LE f1 . p2,f1 . p3,P
by A1, A36, A37, A39, A40, A43, A38, Th51;
A55:
(f1 . p3) `2 < 0
by A9, A20, A22, A33, JGRAPH_4:43;
A56:
|.(f1 . p4).| = 1
by A16, A22, JGRAPH_4:33;
then
f1 . p4 in P
by A1;
then
LE f1 . p3,f1 . p4,P
by A1, A39, A40, A56, A34, A44, A26, Th51;
hence
ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
by A23, A53, A52, A51, A34, A55, A44, A50, A54; verum