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 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & ( p1 `2 >= 0 or p1 `1 >= 0 ) & ( p2 `2 >= 0 or p2 `1 >= 0 ) & ( p3 `2 >= 0 or p3 `1 >= 0 ) & ( p4 `2 > 0 or p4 `1 > 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 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 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 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & ( p1 `2 >= 0 or p1 `1 >= 0 ) & ( p2 `2 >= 0 or p2 `1 >= 0 ) & ( p3 `2 >= 0 or p3 `1 >= 0 ) & ( p4 `2 > 0 or p4 `1 > 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 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 0 & q4 `2 > 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) )
assume A1: ( 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 or p1 `1 >= 0 ) & ( p2 `2 >= 0 or p2 `1 >= 0 ) & ( p3 `2 >= 0 or p3 `1 >= 0 ) & ( p4 `2 > 0 or p4 `1 > 0 ) ) ; :: 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 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 0 & q4 `2 > 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
then A2: P is being_simple_closed_curve by JGRAPH_3:36;
then A3: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1 in P & p2 in P & p3 in P & p4 in P & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P & ( p1 `2 >= 0 or p1 `1 >= 0 ) & ( p2 `2 >= 0 or p2 `1 >= 0 ) & ( p3 `2 >= 0 or p3 `1 >= 0 ) & ( p4 `2 > 0 or p4 `1 > 0 ) ) by A1, JORDAN7:5;
then consider p44 being Point of (TOP-REAL 2) such that
A4: ( p44 = p4 & |.p44.| = 1 ) ;
consider p11 being Point of (TOP-REAL 2) such that
A5: ( p11 = p1 & |.p11.| = 1 ) by A3;
consider p22 being Point of (TOP-REAL 2) such that
A6: ( p22 = p2 & |.p22.| = 1 ) by A3;
consider p33 being Point of (TOP-REAL 2) such that
A7: ( p33 = p3 & |.p33.| = 1 ) by A3;
A8: ( - 1 <= p4 `2 & p4 `2 <= 1 ) by A4, Th3;
now
assume A9: p4 `2 = - 1 ; :: thesis: contradiction
1 ^2 = ((p4 `1 ) ^2 ) + ((p4 `2 ) ^2 ) by A4, JGRAPH_3:10
.= ((p4 `1 ) ^2 ) + 1 by A9 ;
hence contradiction by A1, A9, XCMPLX_1:6; :: thesis: verum
end;
then p4 `2 > - 1 by A8, XXREAL_0:1;
then consider r being real number such that
A10: ( - 1 < r & r < p4 `2 ) by XREAL_1:7;
reconsider r1 = r as Real by XREAL_0:def 1;
A11: ( - 1 < r1 & r1 < 1 ) by A8, A10, XXREAL_0:2;
then consider f1 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A12: ( f1 = r1 -FanMorphE & f1 is being_homeomorphism ) by JGRAPH_4:112;
set q11 = f1 . p1;
set q22 = f1 . p2;
set q33 = f1 . p3;
set q44 = f1 . p4;
A13: |.(f1 . p1).| = 1 by A5, A12, JGRAPH_4:104;
then A14: f1 . p1 in P by A1;
A15: |.(f1 . p2).| = 1 by A6, A12, JGRAPH_4:104;
then A16: f1 . p2 in P by A1;
A17: |.(f1 . p3).| = 1 by A7, A12, JGRAPH_4:104;
then A18: f1 . p3 in P by A1;
A19: |.(f1 . p4).| = 1 by A4, A12, JGRAPH_4:104;
then A20: f1 . p4 in P by A1;
now
per cases ( p4 `2 <= 0 or p4 `2 > 0 ) ;
case A21: p4 `2 <= 0 ; :: 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 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 0 & q4 `2 > 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
A22: (p4 `2 ) / |.p4.| > r1 by A4, A10;
then A23: ( (f1 . p4) `1 > 0 & (f1 . p4) `2 >= 0 ) by A1, A10, A12, A21, JGRAPH_4:113;
A24: now
assume A25: (f1 . p4) `2 = 0 ; :: thesis: contradiction
1 ^2 = (((f1 . p4) `1 ) ^2 ) + (((f1 . p4) `2 ) ^2 ) by A19, JGRAPH_3:10
.= ((f1 . p4) `1 ) ^2 by A25 ;
then ( (f1 . p4) `1 = - 1 or (f1 . p4) `1 = 1 ) by SQUARE_1:110;
then A26: f1 . p4 = |[1,0 ]| by A1, A10, A12, A21, A22, A25, EUCLID:57, JGRAPH_4:113;
set q8 = |[(sqrt (1 - (r1 ^2 ))),r1]|;
A27: ( |[(sqrt (1 - (r1 ^2 ))),r1]| `1 = sqrt (1 - (r1 ^2 )) & |[(sqrt (1 - (r1 ^2 ))),r1]| `2 = r1 ) by EUCLID:56;
then A28: |.|[(sqrt (1 - (r1 ^2 ))),r1]|.| = sqrt (((sqrt (1 - (r1 ^2 ))) ^2 ) + (r1 ^2 )) by JGRAPH_3:10;
1 ^2 > r1 ^2 by A11, SQUARE_1:120;
then A29: 1 - (r1 ^2 ) > 0 by XREAL_1:52;
then A30: |.|[(sqrt (1 - (r1 ^2 ))),r1]|.| = sqrt ((1 - (r1 ^2 )) + (r1 ^2 )) by A28, SQUARE_1:def 4
.= 1 by SQUARE_1:83 ;
then A31: (|[(sqrt (1 - (r1 ^2 ))),r1]| `2 ) / |.|[(sqrt (1 - (r1 ^2 ))),r1]|.| = r1 by EUCLID:56;
A32: |[(sqrt (1 - (r1 ^2 ))),r1]| `1 > 0 by A27, A29, SQUARE_1:93;
set r8 = f1 . |[(sqrt (1 - (r1 ^2 ))),r1]|;
A33: ( (f1 . |[(sqrt (1 - (r1 ^2 ))),r1]|) `1 > 0 & (f1 . |[(sqrt (1 - (r1 ^2 ))),r1]|) `2 = 0 ) by A11, A12, A31, A32, JGRAPH_4:118;
|.(f1 . |[(sqrt (1 - (r1 ^2 ))),r1]|).| = 1 by A12, A30, JGRAPH_4:104;
then 1 ^2 = (((f1 . |[(sqrt (1 - (r1 ^2 ))),r1]|) `1 ) ^2 ) + (((f1 . |[(sqrt (1 - (r1 ^2 ))),r1]|) `2 ) ^2 ) by JGRAPH_3:10
.= ((f1 . |[(sqrt (1 - (r1 ^2 ))),r1]|) `1 ) ^2 by A33 ;
then ( (f1 . |[(sqrt (1 - (r1 ^2 ))),r1]|) `1 = - 1 or (f1 . |[(sqrt (1 - (r1 ^2 ))),r1]|) `1 = 1 ) by SQUARE_1:110;
then A34: f1 . |[(sqrt (1 - (r1 ^2 ))),r1]| = |[1,0 ]| by A33, EUCLID:57;
A35: f1 is one-to-one by A11, A12, JGRAPH_4:109;
dom f1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then p4 = |[(sqrt (1 - (r1 ^2 ))),r1]| by A26, A34, A35, FUNCT_1:def 8;
hence contradiction by A10, EUCLID:56; :: thesis: verum
end;
A36: Lower_Arc P = { p7 where p7 is Point of (TOP-REAL 2) : ( p7 in P & p7 `2 <= 0 ) } by A1, Th38;
A37: Upper_Arc P = { p7 where p7 is Point of (TOP-REAL 2) : ( p7 in P & p7 `2 >= 0 ) } by A1, Th37;
A38: now
per cases ( p3 `1 <= 0 or p3 `1 > 0 ) ;
case A39: p3 `1 <= 0 ; :: thesis: ( (f1 . p1) `2 >= 0 & (f1 . p2) `2 >= 0 & (f1 . p3) `2 >= 0 & (f1 . p4) `2 > 0 & LE f1 . p1,f1 . p2,P & LE f1 . p2,f1 . p3,P & LE f1 . p3,f1 . p4,P )
then A40: f1 . p3 = p3 by A12, JGRAPH_4:89;
A41: now
per cases ( p3 `1 = 0 or p3 `1 < 0 ) by A39;
case p3 `1 = 0 ; :: thesis: (f1 . p3) `2 >= 0
then A42: 1 ^2 = (0 ^2 ) + (((f1 . p3) `2 ) ^2 ) by A7, A40, JGRAPH_3:10
.= ((f1 . p3) `2 ) ^2 ;
now
assume (f1 . p3) `2 = - 1 ; :: thesis: contradiction
then - 1 >= p4 `2 by A1, A21, A40, Th53;
hence contradiction by A10, XXREAL_0:2; :: thesis: verum
end;
hence (f1 . p3) `2 >= 0 by A42, SQUARE_1:110; :: thesis: verum
end;
case p3 `1 < 0 ; :: thesis: (f1 . p3) `2 >= 0
hence (f1 . p3) `2 >= 0 by A1, A12, JGRAPH_4:89; :: thesis: verum
end;
end;
end;
now
per cases ( p2 <> W-min P or p2 = W-min P ) ;
case A43: p2 <> W-min P ; :: thesis: ( (f1 . p1) `2 >= 0 & (f1 . p2) `2 >= 0 & (f1 . p3) `2 >= 0 & (f1 . p4) `2 > 0 & LE f1 . p1,f1 . p2,P & LE f1 . p2,f1 . p3,P & LE f1 . p3,f1 . p4,P )
then A47: p2 `1 <= p3 `1 by A1, A40, A41, Th50;
then A48: f1 . p2 = p2 by A12, A39, JGRAPH_4:89;
now
per cases ( p1 <> W-min P or p1 = W-min P ) ;
case A49: p1 <> W-min P ; :: thesis: ( (f1 . p1) `2 >= 0 & (f1 . p2) `2 >= 0 & (f1 . p3) `2 >= 0 & (f1 . p4) `2 > 0 & LE f1 . p1,f1 . p2,P & LE f1 . p2,f1 . p3,P & LE f1 . p3,f1 . p4,P )
then p1 `1 <= p2 `1 by A1, A44, Th50;
hence ( (f1 . p1) `2 >= 0 & (f1 . p2) `2 >= 0 & (f1 . p3) `2 >= 0 & (f1 . p4) `2 > 0 & LE f1 . p1,f1 . p2,P & LE f1 . p2,f1 . p3,P & LE f1 . p3,f1 . p4,P ) by A1, A12, A18, A20, A23, A24, A40, A41, A44, A47, A48, A50, Th57, JGRAPH_4:89; :: thesis: verum
end;
case A53: p1 = W-min P ; :: thesis: ( (f1 . p1) `2 >= 0 & (f1 . p2) `2 >= 0 & (f1 . p3) `2 >= 0 & (f1 . p4) `2 > 0 & LE f1 . p1,f1 . p2,P & LE f1 . p2,f1 . p3,P & LE f1 . p3,f1 . p4,P )
A54: W-min P = |[(- 1),0 ]| by A1, Th32;
then ( p1 `1 = - 1 & p1 `2 = 0 ) by A53, EUCLID:56;
then p1 = f1 . p1 by A12, JGRAPH_4:89;
hence ( (f1 . p1) `2 >= 0 & (f1 . p2) `2 >= 0 & (f1 . p3) `2 >= 0 & (f1 . p4) `2 > 0 & LE f1 . p1,f1 . p2,P & LE f1 . p2,f1 . p3,P & LE f1 . p3,f1 . p4,P ) by A3, A12, A20, A23, A24, A40, A41, A44, A47, A53, A54, Th57, EUCLID:56, JGRAPH_4:89; :: thesis: verum
end;
end;
end;
hence ( (f1 . p1) `2 >= 0 & (f1 . p2) `2 >= 0 & (f1 . p3) `2 >= 0 & (f1 . p4) `2 > 0 & LE f1 . p1,f1 . p2,P & LE f1 . p2,f1 . p3,P & LE f1 . p3,f1 . p4,P ) ; :: thesis: verum
end;
case A55: p2 = W-min P ; :: thesis: ( (f1 . p1) `2 >= 0 & (f1 . p2) `2 >= 0 & (f1 . p3) `2 >= 0 & (f1 . p4) `2 > 0 & LE f1 . p1,f1 . p2,P & LE f1 . p2,f1 . p3,P & LE f1 . p3,f1 . p4,P )
A56: W-min P = |[(- 1),0 ]| by A1, Th32;
then A57: ( p2 `1 = - 1 & p2 `2 = 0 ) by A55, EUCLID:56;
then A58: p2 = f1 . p2 by A12, JGRAPH_4:89;
then p1 `1 <= p2 `1 by A1, A57, Th50;
hence ( (f1 . p1) `2 >= 0 & (f1 . p2) `2 >= 0 & (f1 . p3) `2 >= 0 & (f1 . p4) `2 > 0 & LE f1 . p1,f1 . p2,P & LE f1 . p2,f1 . p3,P & LE f1 . p3,f1 . p4,P ) by A1, A10, A12, A18, A20, A21, A23, A24, A40, A41, A57, A58, Th57, JGRAPH_4:89; :: thesis: verum
end;
end;
end;
hence ( (f1 . p1) `2 >= 0 & (f1 . p2) `2 >= 0 & (f1 . p3) `2 >= 0 & (f1 . p4) `2 > 0 & LE f1 . p1,f1 . p2,P & LE f1 . p2,f1 . p3,P & LE f1 . p3,f1 . p4,P ) ; :: thesis: verum
end;
case A63: p3 `1 > 0 ; :: thesis: ( (f1 . p1) `2 >= 0 & (f1 . p2) `2 >= 0 & (f1 . p3) `2 >= 0 & (f1 . p4) `2 > 0 & LE f1 . p1,f1 . p2,P & LE f1 . p2,f1 . p3,P & LE f1 . p3,f1 . p4,P )
A64: now
per cases ( p3 <> p4 or p3 = p4 ) ;
case A65: p3 <> p4 ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P & (f1 . p3) `2 >= 0 & LE f1 . p3,f1 . p4,P )
then p3 `2 > p4 `2 by A1, A21, A63, Th53;
then A66: (p3 `2 ) / |.p3.| >= r1 by A7, A10, XXREAL_0:2;
then A67: ( (f1 . p3) `1 > 0 & (f1 . p3) `2 >= 0 ) by A11, A12, A63, JGRAPH_4:113;
(p3 `2 ) / |.p3.| > (p4 `2 ) / |.p4.| by A1, A4, A7, A21, A63, A65, Th53;
then A68: ((f1 . p3) `2 ) / |.(f1 . p3).| > ((f1 . p4) `2 ) / |.(f1 . p4).| by A1, A4, A7, A10, A12, A21, A63, Th27;
A69: 1 ^2 = (((f1 . p3) `1 ) ^2 ) + (((f1 . p3) `2 ) ^2 ) by A17, JGRAPH_3:10;
then A70: (f1 . p3) `1 = sqrt ((1 ^2 ) - (((f1 . p3) `2 ) ^2 )) by A67, SQUARE_1:89;
1 ^2 = (((f1 . p4) `1 ) ^2 ) + (((f1 . p4) `2 ) ^2 ) by A19, JGRAPH_3:10;
then A71: (f1 . p4) `1 = sqrt ((1 ^2 ) - (((f1 . p4) `2 ) ^2 )) by A23, SQUARE_1:89;
((f1 . p3) `2 ) ^2 > ((f1 . p4) `2 ) ^2 by A17, A19, A23, A68, SQUARE_1:78;
then (1 ^2 ) - (((f1 . p3) `2 ) ^2 ) < (1 ^2 ) - (((f1 . p4) `2 ) ^2 ) by XREAL_1:17;
then A72: (f1 . p3) `1 < (f1 . p4) `1 by A69, A70, A71, SQUARE_1:95, XREAL_1:65;
A73: now
assume p2 `1 = 0 ; :: thesis: ( p2 `2 = 1 or p2 `2 = - 1 )
then 1 ^2 = (0 ^2 ) + ((p2 `2 ) ^2 ) by A6, JGRAPH_3:10;
hence ( p2 `2 = 1 or p2 `2 = - 1 ) by SQUARE_1:109; :: thesis: verum
end;
A74: now
assume A75: ( p2 `1 = 0 & p2 `2 = - 1 ) ; :: thesis: contradiction
then p2 `2 <= p4 `2 by A4, Th3;
then A76: LE p4,p2,P by A3, A21, A75, Th58;
LE p2,p4,P by A1, JGRAPH_3:36, JORDAN6:73;
hence contradiction by A1, A75, A76, JGRAPH_3:36, JORDAN6:72; :: thesis: verum
end;
now
per cases ( ( p2 `1 <= 0 & p2 `2 >= 0 ) or p2 `1 > 0 ) by A1, A73, A74;
case A77: ( p2 `1 <= 0 & p2 `2 >= 0 ) ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )
then f1 . p2 = p2 by A12, JGRAPH_4:89;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) by A3, A18, A67, A77, Th57; :: thesis: verum
end;
case A78: p2 `1 > 0 ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )
then A79: (f1 . p2) `1 > 0 by A11, A12, Th25;
now
per cases ( p2 = p3 or p2 <> p3 ) ;
case p2 = p3 ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) by A2, A11, A12, A18, A63, A66, JGRAPH_4:113, JORDAN6:71; :: thesis: verum
end;
case p2 <> p3 ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )
then (p2 `2 ) / |.p2.| > (p3 `2 ) / |.p3.| by A1, A6, A7, A63, A78, Th53;
then ((f1 . p2) `2 ) / |.(f1 . p2).| > ((f1 . p3) `2 ) / |.(f1 . p3).| by A6, A7, A11, A12, A63, A78, Th27;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) by A1, A15, A16, A17, A18, A67, A79, Th58; :: thesis: verum
end;
end;
end;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) ; :: thesis: verum
end;
end;
end;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P & (f1 . p3) `2 >= 0 & LE f1 . p3,f1 . p4,P ) by A1, A18, A20, A23, A67, A72, Th57; :: thesis: verum
end;
case A80: p3 = p4 ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P & (f1 . p3) `2 >= 0 & LE f1 . p3,f1 . p4,P )
then A81: (p3 `2 ) / |.p3.| >= r1 by A7, A10;
then A82: ( (f1 . p3) `1 > 0 & (f1 . p3) `2 >= 0 ) by A11, A12, A63, JGRAPH_4:113;
A83: now
assume p2 `1 = 0 ; :: thesis: ( p2 `2 = 1 or p2 `2 = - 1 )
then 1 ^2 = (0 ^2 ) + ((p2 `2 ) ^2 ) by A6, JGRAPH_3:10;
hence ( p2 `2 = 1 or p2 `2 = - 1 ) by SQUARE_1:109; :: thesis: verum
end;
A84: now
assume A85: ( p2 `1 = 0 & p2 `2 = - 1 ) ; :: thesis: contradiction
then A86: LE p4,p2,P by A3, A8, A21, Th58;
LE p2,p4,P by A1, JGRAPH_3:36, JORDAN6:73;
hence contradiction by A1, A85, A86, JGRAPH_3:36, JORDAN6:72; :: thesis: verum
end;
now
per cases ( ( p2 `1 <= 0 & p2 `2 >= 0 ) or p2 `1 > 0 ) by A1, A83, A84;
case A87: ( p2 `1 <= 0 & p2 `2 >= 0 ) ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )
then f1 . p2 = p2 by A12, JGRAPH_4:89;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) by A3, A18, A82, A87, Th57; :: thesis: verum
end;
case A88: p2 `1 > 0 ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )
then A89: (f1 . p2) `1 > 0 by A11, A12, Th25;
now
per cases ( p2 = p3 or p2 <> p3 ) ;
case p2 = p3 ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) by A2, A11, A12, A18, A63, A81, JGRAPH_4:113, JORDAN6:71; :: thesis: verum
end;
case p2 <> p3 ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )
then (p2 `2 ) / |.p2.| > (p3 `2 ) / |.p3.| by A1, A6, A7, A63, A88, Th53;
then ((f1 . p2) `2 ) / |.(f1 . p2).| > ((f1 . p3) `2 ) / |.(f1 . p3).| by A6, A7, A11, A12, A63, A88, Th27;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) by A1, A15, A16, A17, A18, A82, A89, Th58; :: thesis: verum
end;
end;
end;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) ; :: thesis: verum
end;
end;
end;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P & (f1 . p3) `2 >= 0 & LE f1 . p3,f1 . p4,P ) by A1, A18, A23, A80, Th57; :: thesis: verum
end;
end;
end;
A90: now
assume p1 `1 = 0 ; :: thesis: ( p1 `2 = 1 or p1 `2 = - 1 )
then 1 ^2 = (0 ^2 ) + ((p1 `2 ) ^2 ) by A5, JGRAPH_3:10;
hence ( p1 `2 = 1 or p1 `2 = - 1 ) by SQUARE_1:109; :: thesis: verum
end;
A91: now
assume A92: ( p1 `1 = 0 & p1 `2 = - 1 ) ; :: thesis: contradiction
then A93: LE p4,p1,P by A3, A8, A21, Th58;
LE p1,p3,P by A1, JGRAPH_3:36, JORDAN6:73;
then LE p1,p4,P by A1, JGRAPH_3:36, JORDAN6:73;
hence contradiction by A1, A92, A93, JGRAPH_3:36, JORDAN6:72; :: thesis: verum
end;
A94: now
assume p2 `1 = 0 ; :: thesis: ( p2 `2 = 1 or p2 `2 = - 1 )
then 1 ^2 = (0 ^2 ) + ((p2 `2 ) ^2 ) by A6, JGRAPH_3:10;
hence ( p2 `2 = 1 or p2 `2 = - 1 ) by SQUARE_1:109; :: thesis: verum
end;
A95: now
assume A96: ( p2 `1 = 0 & p2 `2 = - 1 ) ; :: thesis: contradiction
then p2 `2 <= p4 `2 by A4, Th3;
then A97: LE p4,p2,P by A3, A21, A96, Th58;
LE p2,p4,P by A1, JGRAPH_3:36, JORDAN6:73;
hence contradiction by A1, A96, A97, JGRAPH_3:36, JORDAN6:72; :: thesis: verum
end;
now
per cases ( ( p1 `1 <= 0 & p1 `2 >= 0 ) or p1 `1 > 0 ) by A1, A90, A91;
case A98: ( p1 `1 <= 0 & p1 `2 >= 0 ) ; :: thesis: ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )
then A99: p1 = f1 . p1 by A12, JGRAPH_4:89;
A100: (f1 . p1) `2 >= 0 by A12, A98, JGRAPH_4:89;
now
per cases ( ( p2 `1 <= 0 & p2 `2 >= 0 ) or p2 `1 > 0 ) by A1, A94, A95;
case ( p2 `1 <= 0 & p2 `2 >= 0 ) ; :: thesis: ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )
hence ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) by A1, A12, A98, A99, JGRAPH_4:89; :: thesis: verum
end;
case p2 `1 > 0 ; :: thesis: ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )
then (f1 . p1) `1 < (f1 . p2) `1 by A11, A12, A98, A99, Th25;
hence ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) by A1, A14, A16, A64, A100, Th57; :: thesis: verum
end;
end;
end;
hence ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) ; :: thesis: verum
end;
case A101: p1 `1 > 0 ; :: thesis: ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )
then A102: (f1 . p1) `1 > 0 by A11, A12, Th25;
now
per cases ( ( p2 `1 <= 0 & p2 `2 >= 0 ) or p2 `1 > 0 ) by A1, A94, A95;
case A103: ( p2 `1 <= 0 & p2 `2 >= 0 ) ; :: thesis: ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )
then LE p2,p1,P by A3, A101, A103, Th57;
then f1 . p1 = f1 . p2 by A1, JGRAPH_3:36, JORDAN6:72;
hence ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) by A2, A12, A14, A103, JGRAPH_4:89, JORDAN6:71; :: thesis: verum
end;
case A107: p2 `1 > 0 ; :: thesis: ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )
then A108: (f1 . p2) `1 > 0 by A11, A12, Th25;
now
per cases ( p1 = p2 or p1 <> p2 ) ;
case p1 = p2 ; :: thesis: ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )
hence ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) by A1, A14, A64, JGRAPH_3:36, JORDAN6:71; :: thesis: verum
end;
case p1 <> p2 ; :: thesis: ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )
then (p1 `2 ) / |.p1.| > (p2 `2 ) / |.p2.| by A1, A5, A6, A101, A107, Th53;
then ((f1 . p1) `2 ) / |.(f1 . p1).| > ((f1 . p2) `2 ) / |.(f1 . p2).| by A5, A6, A11, A12, A101, A107, Th27;
hence ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) by A1, A13, A14, A15, A16, A64, A102, A108, Th58; :: thesis: verum
end;
end;
end;
hence ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) ; :: thesis: verum
end;
end;
end;
hence ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) ; :: thesis: verum
end;
end;
end;
hence ( (f1 . p1) `2 >= 0 & (f1 . p2) `2 >= 0 & (f1 . p3) `2 >= 0 & (f1 . p4) `2 > 0 & LE f1 . p1,f1 . p2,P & LE f1 . p2,f1 . p3,P & LE f1 . p3,f1 . p4,P ) by A1, A10, A12, A21, A22, A24, A64, JGRAPH_4:113; :: thesis: verum
end;
end;
end;
for q being Point of (TOP-REAL 2) holds |.(f1 . q).| = |.q.| by A12, JGRAPH_4:104;
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 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 0 & q4 `2 > 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) by A12, A38; :: thesis: verum
end;
case A109: p4 `2 > 0 ; :: 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 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 0 & q4 `2 > 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
A110: ( ( p3 in Upper_Arc P & p4 in Lower_Arc P & not p4 = W-min P ) or ( p3 in Upper_Arc P & p4 in Upper_Arc P & LE p3,p4, Upper_Arc P, W-min P, E-max P ) or ( p3 in Lower_Arc P & p4 in Lower_Arc P & not p4 = W-min P & LE p3,p4, Lower_Arc P, E-max P, W-min P ) ) by A1, JORDAN6:def 10;
A111: Upper_Arc P = { p7 where p7 is Point of (TOP-REAL 2) : ( p7 in P & p7 `2 >= 0 ) } by A1, Th37;
A112: Lower_Arc P = { p8 where p8 is Point of (TOP-REAL 2) : ( p8 in P & p8 `2 <= 0 ) } by A1, Th38;
A113: now
assume p4 in Lower_Arc P ; :: thesis: contradiction
then consider p9 being Point of (TOP-REAL 2) such that
A114: ( p9 = p4 & p9 in P & p9 `2 <= 0 ) by A112;
thus contradiction by A109, A114; :: thesis: verum
end;
then consider p33 being Point of (TOP-REAL 2) such that
A115: ( p33 = p3 & p33 in P & p33 `2 >= 0 ) by A110, A111;
A116: LE p2,p4,P by A1, JGRAPH_3:36, JORDAN6:73;
then ( ( p2 in Upper_Arc P & p4 in Lower_Arc P & not p4 = W-min P ) or ( p2 in Upper_Arc P & p4 in Upper_Arc P & LE p2,p4, Upper_Arc P, W-min P, E-max P ) or ( p2 in Lower_Arc P & p4 in Lower_Arc P & not p4 = W-min P & LE p2,p4, Lower_Arc P, E-max P, W-min P ) ) by JORDAN6:def 10;
then consider p22 being Point of (TOP-REAL 2) such that
A117: ( p22 = p2 & p22 in P & p22 `2 >= 0 ) by A111, A113;
LE p1,p4,P by A1, A116, JGRAPH_3:36, JORDAN6:73;
then ( ( p1 in Upper_Arc P & p4 in Lower_Arc P & not p4 = W-min P ) or ( p1 in Upper_Arc P & p4 in Upper_Arc P & LE p1,p4, Upper_Arc P, W-min P, E-max P ) or ( p1 in Lower_Arc P & p4 in Lower_Arc P & not p4 = W-min P & LE p1,p4, Lower_Arc P, E-max P, W-min P ) ) by JORDAN6:def 10;
then consider p11 being Point of (TOP-REAL 2) such that
A118: ( p11 = p1 & p11 in P & p11 `2 >= 0 ) by A111, A113;
set f4 = id (TOP-REAL 2);
A119: ( (id (TOP-REAL 2)) . p1 = p1 & (id (TOP-REAL 2)) . p2 = p2 & (id (TOP-REAL 2)) . p3 = p3 & (id (TOP-REAL 2)) . p4 = p4 ) by FUNCT_1:35;
for q being Point of (TOP-REAL 2) holds |.((id (TOP-REAL 2)) . q).| = |.q.| by FUNCT_1:35;
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 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 0 & q4 `2 > 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) by A1, A109, A115, A117, A118, A119; :: thesis: verum
end;
end;
end;
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 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 0 & q4 `2 > 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) ; :: thesis: verum