let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p4 = W-min P & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P 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); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p4 = W-min P & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P 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: p4 = W-min P and
A3: LE p1,p2,P and
A4: LE p2,p3,P and
A5: LE p3,p4,P ; :: thesis: 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 )
A6: Upper_Arc P = { p7 where p7 is Point of (TOP-REAL 2) : ( p7 in P & p7 `2 >= 0 ) } by A1, Th34;
A7: W-min P = |[(- 1),0]| by A1, Th29;
then A8: (W-min P) `2 = 0 by EUCLID:52;
A9: P is being_simple_closed_curve by A1, JGRAPH_3:26;
then p4 in P by A5, JORDAN7:5;
then A10: p4 in Upper_Arc P by A2, A6, A8;
A11: Upper_Arc P is_an_arc_of W-min P, E-max P by A9, JORDAN6:def 8;
A12: p3 in Upper_Arc P by A1, A5, A10, Th44;
then LE p4,p3, Upper_Arc P, W-min P, E-max P by A2, A11, JORDAN5C:10;
then LE p4,p3,P by A10, A12;
then A13: p3 = p4 by A1, A5, JGRAPH_3:26, JORDAN6:57;
A14: LE p2,p4,P by A1, A4, A5, JGRAPH_3:26, JORDAN6:58;
A15: p2 in Upper_Arc P by A1, A4, A12, Th44;
then LE p4,p2, Upper_Arc P, W-min P, E-max P by A2, A11, JORDAN5C:10;
then LE p4,p2,P by A10, A15;
then A16: p2 = p4 by A1, A14, JGRAPH_3:26, JORDAN6:57;
A17: (W-min P) `1 = - 1 by A7, EUCLID:52;
A18: p1 in Upper_Arc P by A1, A3, A15, Th44;
then LE p4,p1, Upper_Arc P, W-min P, E-max P by A2, A11, JORDAN5C:10;
then LE p4,p1,P by A10, A18;
then p1 = p4 by A1, A3, A16, JGRAPH_3:26, JORDAN6:57;
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 A1, A2, A3, A17, A8, A13, A16, Th59; :: thesis: verum