let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis:
let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
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 ; :: thesis:
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; :: thesis: