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 `2 >= 0 & p2 `2 >= 0 & p3 `2 >= 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 `2 >= 0 & p2 `2 >= 0 & p3 `2 >= 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 `2 >= 0
and
A6:
p2 `2 >= 0
and
A7:
p3 `2 >= 0
and
A8:
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 )
A9:
P is being_simple_closed_curve
by A1, JGRAPH_3:26;
then
p4 in P
by A4, JORDAN7:5;
then A10:
ex p being Point of (TOP-REAL 2) st
( p = p4 & |.p.| = 1 )
by A1;
p4 `1 <= 1
by A10, Th1;
then
p4 `1 < 1
by A11, XXREAL_0:1;
then consider r being Real such that
A12:
p4 `1 < r
and
A13:
r < 1
by XREAL_1:5;
reconsider r1 = r as Real ;
- 1 <= p4 `1
by A10, Th1;
then A14:
- 1 < r1
by A12, XXREAL_0:2;
then consider f1 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A15:
f1 = r1 -FanMorphN
and
A16:
f1 is being_homeomorphism
by A13, JGRAPH_4:74;
set q11 = f1 . p1;
set q22 = f1 . p2;
set q33 = f1 . p3;
set q44 = f1 . p4;
A17:
for q being Point of (TOP-REAL 2) holds |.(f1 . q).| = |.q.|
by A15, JGRAPH_4:66;
A18:
( p3 `1 < p4 `1 or p3 = p4 )
by A1, A4, A8, Th47;
then A19:
p3 `1 < r1
by A12, XXREAL_0:2;
p3 in P
by A3, A9, JORDAN7:5;
then A20:
ex p33 being Point of (TOP-REAL 2) st
( p33 = p3 & |.p33.| = 1 )
by A1;
then
( (p3 `1) / |.p3.| < (p4 `1) / |.p4.| or p3 = p4 )
by A1, A4, A8, A10, Th47;
then A21:
( ((f1 . p3) `1) / |.(f1 . p3).| < ((f1 . p4) `1) / |.(f1 . p4).| or p3 = p4 )
by A7, A8, A10, A20, A13, A14, A15, Th21;
A22:
(p3 `1) / |.p3.| < r1
by A20, A12, A18, XXREAL_0:2;
then A23:
(f1 . p3) `2 >= 0
by A7, A20, A13, A14, A15, Th20;
A24:
( p1 `1 < p2 `1 or p1 = p2 )
by A1, A2, A6, Th47;
(p4 `1) / |.p4.| < r1
by A10, A12;
then A25:
( (f1 . p4) `1 < 0 & (f1 . p4) `2 > 0 )
by A8, A14, A15, JGRAPH_4:76;
p2 in P
by A2, A9, JORDAN7:5;
then A26:
ex p22 being Point of (TOP-REAL 2) st
( p22 = p2 & |.p22.| = 1 )
by A1;
then A27:
|.(f1 . p2).| = 1
by A15, JGRAPH_4:66;
then A28:
f1 . p2 in P
by A1;
A29:
( p2 `1 < p3 `1 or p2 = p3 )
by A1, A3, A7, Th47;
then A30:
(p2 `1) / |.p2.| < r1
by A26, A19, XXREAL_0:2;
then A31:
(f1 . p2) `2 >= 0
by A6, A26, A13, A14, A15, Th20;
p1 in P
by A2, A9, JORDAN7:5;
then A32:
ex p11 being Point of (TOP-REAL 2) st
( p11 = p1 & |.p11.| = 1 )
by A1;
then
( (p1 `1) / |.p1.| < (p2 `1) / |.p2.| or p1 = p2 )
by A1, A2, A6, A26, Th47;
then A33:
( ((f1 . p1) `1) / |.(f1 . p1).| < ((f1 . p2) `1) / |.(f1 . p2).| or p1 = p2 )
by A5, A6, A32, A26, A13, A14, A15, Th21;
p2 `1 < r1
by A29, A19, XXREAL_0:2;
then A34:
(p1 `1) / |.p1.| < r1
by A32, A24, XXREAL_0:2;
then A35:
(f1 . p1) `2 >= 0
by A5, A32, A13, A14, A15, Th20;
A36:
(f1 . p2) `1 < 0
by A6, A26, A13, A14, A15, A30, Th20;
A37:
|.(f1 . p1).| = 1
by A32, A15, JGRAPH_4:66;
then
f1 . p1 in P
by A1;
then A38:
LE f1 . p1,f1 . p2,P
by A1, A37, A27, A28, A31, A36, A35, A33, Th53;
A39:
|.(f1 . p3).| = 1
by A20, A15, JGRAPH_4:66;
then A40:
f1 . p3 in P
by A1;
A41:
(f1 . p3) `1 < 0
by A7, A20, A13, A14, A15, A22, Th20;
A42:
( (f1 . p2) `1 < 0 & (f1 . p2) `2 >= 0 )
by A6, A26, A13, A14, A15, A30, Th20;
A43:
( ( (f1 . p1) `1 < 0 & (f1 . p1) `2 >= 0 ) or ( (f1 . p1) `1 < 0 & (f1 . p1) `2 = 0 ) )
by A5, A32, A13, A14, A15, A34, Th20;
A44:
|.(f1 . p4).| = 1
by A10, A15, JGRAPH_4:66;
then
f1 . p4 in P
by A1;
then A45:
LE f1 . p3,f1 . p4,P
by A1, A39, A40, A44, A25, A23, A21, Th53;
( (p2 `1) / |.p2.| < (p3 `1) / |.p3.| or p2 = p3 )
by A1, A3, A7, A26, A20, Th47;
then
( ((f1 . p2) `1) / |.(f1 . p2).| < ((f1 . p3) `1) / |.(f1 . p3).| or p2 = p3 )
by A6, A7, A26, A20, A13, A14, A15, Th21;
then
LE f1 . p2,f1 . p3,P
by A1, A27, A28, A39, A40, A31, A23, A41, Th53;
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 A16, A17, A25, A43, A42, A38, A23, A41, A45; verum