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 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 or p1 `1 >= 0 ) and
A6: ( p2 `2 >= 0 or p2 `1 >= 0 ) and
A7: ( p3 `2 >= 0 or p3 `1 >= 0 ) and
A8: ( 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 )
A9: P is being_simple_closed_curve by A1, JGRAPH_3:26;
then A10: p4 in P by A4, JORDAN7:5;
then A11: ex p44 being Point of (TOP-REAL 2) st
( p44 = p4 & |.p44.| = 1 ) by A1;
then A12: - 1 <= p4 `2 by Th1;
now :: thesis: not p4 `2 = - 1
assume A13: p4 `2 = - 1 ; :: thesis: contradiction
1 ^2 = ((p4 `1) ^2) + ((p4 `2) ^2) by A11, JGRAPH_3:1
.= ((p4 `1) ^2) + 1 by A13 ;
hence contradiction by A8, A13, XCMPLX_1:6; :: thesis: verum
end;
then p4 `2 > - 1 by A12, XXREAL_0:1;
then consider r being Real such that
A14: - 1 < r and
A15: r < p4 `2 by XREAL_1:5;
reconsider r1 = r as Real ;
p4 `2 <= 1 by A11, Th1;
then A16: r1 < 1 by A15, XXREAL_0:2;
then consider f1 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A17: f1 = r1 -FanMorphE and
A18: f1 is being_homeomorphism by A14, JGRAPH_4:105;
set q11 = f1 . p1;
set q22 = f1 . p2;
set q33 = f1 . p3;
set q44 = f1 . p4;
A19: |.(f1 . p4).| = 1 by A11, A17, JGRAPH_4:97;
then A20: f1 . p4 in P by A1;
A21: p1 in P by A2, A9, JORDAN7:5;
then A22: ex p11 being Point of (TOP-REAL 2) st
( p11 = p1 & |.p11.| = 1 ) by A1;
then A23: |.(f1 . p1).| = 1 by A17, JGRAPH_4:97;
then A24: f1 . p1 in P by A1;
A25: p3 in P by A3, A9, JORDAN7:5;
then A26: ex p33 being Point of (TOP-REAL 2) st
( p33 = p3 & |.p33.| = 1 ) by A1;
then A27: |.(f1 . p3).| = 1 by A17, JGRAPH_4:97;
then A28: f1 . p3 in P by A1;
A29: p2 in P by A2, A9, JORDAN7:5;
then A30: ex p22 being Point of (TOP-REAL 2) st
( p22 = p2 & |.p22.| = 1 ) by A1;
then A31: |.(f1 . p2).| = 1 by A17, JGRAPH_4:97;
then A32: f1 . p2 in P by A1;
now :: thesis: ( ( 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 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 0 & q4 `2 > 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) ) or ( 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 `2 >= 0 & q2 `2 >= 0 & q3 `2 >= 0 & q4 `2 > 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) ) )
per cases ( p4 `2 <= 0 or p4 `2 > 0 ) ;
case A33: 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 )
A34: Upper_Arc P = { p7 where p7 is Point of (TOP-REAL 2) : ( p7 in P & p7 `2 >= 0 ) } by A1, Th34;
A35: (p4 `2) / |.p4.| > r1 by A11, A15;
then A36: (f1 . p4) `1 > 0 by A8, A15, A17, A33, JGRAPH_4:106;
A37: now :: thesis: not (f1 . p4) `2 = 0
set q8 = |[(sqrt (1 - (r1 ^2))),r1]|;
assume A38: (f1 . p4) `2 = 0 ; :: thesis: contradiction
1 ^2 = (((f1 . p4) `1) ^2) + (((f1 . p4) `2) ^2) by A19, JGRAPH_3:1
.= ((f1 . p4) `1) ^2 by A38 ;
then ( (f1 . p4) `1 = - 1 or (f1 . p4) `1 = 1 ) by SQUARE_1:41;
then A39: f1 . p4 = |[1,0]| by A8, A15, A17, A33, A35, A38, EUCLID:53, JGRAPH_4:106;
set r8 = f1 . |[(sqrt (1 - (r1 ^2))),r1]|;
1 ^2 > r1 ^2 by A14, A16, SQUARE_1:50;
then A40: 1 - (r1 ^2) > 0 by XREAL_1:50;
A41: |[(sqrt (1 - (r1 ^2))),r1]| `1 = sqrt (1 - (r1 ^2)) by EUCLID:52;
then A42: |[(sqrt (1 - (r1 ^2))),r1]| `1 > 0 by A40, SQUARE_1:25;
|[(sqrt (1 - (r1 ^2))),r1]| `2 = r1 by EUCLID:52;
then |.|[(sqrt (1 - (r1 ^2))),r1]|.| = sqrt (((sqrt (1 - (r1 ^2))) ^2) + (r1 ^2)) by A41, JGRAPH_3:1;
then A43: |.|[(sqrt (1 - (r1 ^2))),r1]|.| = sqrt ((1 - (r1 ^2)) + (r1 ^2)) by A40, SQUARE_1:def 2
.= 1 ;
then A44: (|[(sqrt (1 - (r1 ^2))),r1]| `2) / |.|[(sqrt (1 - (r1 ^2))),r1]|.| = r1 by EUCLID:52;
then A45: (f1 . |[(sqrt (1 - (r1 ^2))),r1]|) `2 = 0 by A17, A42, JGRAPH_4:111;
|.(f1 . |[(sqrt (1 - (r1 ^2))),r1]|).| = 1 by A17, A43, JGRAPH_4:97;
then 1 ^2 = (((f1 . |[(sqrt (1 - (r1 ^2))),r1]|) `1) ^2) + (((f1 . |[(sqrt (1 - (r1 ^2))),r1]|) `2) ^2) by JGRAPH_3:1
.= ((f1 . |[(sqrt (1 - (r1 ^2))),r1]|) `1) ^2 by A45 ;
then ( (f1 . |[(sqrt (1 - (r1 ^2))),r1]|) `1 = - 1 or (f1 . |[(sqrt (1 - (r1 ^2))),r1]|) `1 = 1 ) by SQUARE_1:41;
then A46: f1 . |[(sqrt (1 - (r1 ^2))),r1]| = |[1,0]| by A17, A44, A42, A45, EUCLID:53, JGRAPH_4:111;
( f1 is one-to-one & dom f1 = the carrier of (TOP-REAL 2) ) by A14, A16, A17, FUNCT_2:def 1, JGRAPH_4:102;
then p4 = |[(sqrt (1 - (r1 ^2))),r1]| by A39, A46, FUNCT_1:def 4;
hence contradiction by A15, EUCLID:52; :: thesis: verum
end;
A47: (f1 . p4) `2 >= 0 by A8, A15, A17, A33, A35, JGRAPH_4:106;
A48: Lower_Arc P = { p7 where p7 is Point of (TOP-REAL 2) : ( p7 in P & p7 `2 <= 0 ) } by A1, Th35;
A49: now :: thesis: ( ( p3 `1 <= 0 & (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 ) or ( p3 `1 > 0 & (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 ) )
per cases ( p3 `1 <= 0 or p3 `1 > 0 ) ;
case A50: 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 A51: f1 . p3 = p3 by A17, JGRAPH_4:82;
A52: now :: thesis: ( ( p3 `1 = 0 & (f1 . p3) `2 >= 0 ) or ( p3 `1 < 0 & (f1 . p3) `2 >= 0 ) )
per cases ( p3 `1 = 0 or p3 `1 < 0 ) by A50;
case A53: p3 `1 = 0 ; :: thesis: (f1 . p3) `2 >= 0
A54: now :: thesis: not (f1 . p3) `2 = - 1
assume (f1 . p3) `2 = - 1 ; :: thesis: contradiction
then - 1 >= p4 `2 by A1, A4, A7, A8, A33, A51, Th50;
hence contradiction by A14, A15, XXREAL_0:2; :: thesis: verum
end;
1 ^2 = (0 ^2) + (((f1 . p3) `2) ^2) by A26, A51, A53, JGRAPH_3:1
.= ((f1 . p3) `2) ^2 ;
hence (f1 . p3) `2 >= 0 by A54, SQUARE_1:41; :: thesis: verum
end;
case p3 `1 < 0 ; :: thesis: (f1 . p3) `2 >= 0
hence (f1 . p3) `2 >= 0 by A7, A17, JGRAPH_4:82; :: thesis: verum
end;
end;
end;
now :: thesis: ( ( p2 <> W-min P & (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 ) or ( p2 = W-min P & (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 ) )
per cases ( p2 <> W-min P or p2 = W-min P ) ;
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 )
A59: p2 `1 <= p3 `1 by A1, A3, A51, A52, Th47;
then A60: f1 . p2 = p2 by A17, A50, JGRAPH_4:82;
now :: thesis: ( ( p1 <> W-min P & (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 ) or ( p1 = W-min P & (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 ) )
per cases ( p1 <> W-min P or p1 = W-min P ) ;
case A61: 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 )
p1 `1 <= p2 `1 by A1, A2, A56, Th47;
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, A2, A3, A17, A28, A20, A36, A47, A37, A51, A52, A56, A59, A60, A62, Th54, JGRAPH_4:82; :: thesis: verum
end;
case A65: 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 )
A66: W-min P = |[(- 1),0]| by A1, Th29;
then p1 `1 = - 1 by A65, EUCLID:52;
then p1 = f1 . p1 by A17, JGRAPH_4:82;
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, A2, A3, A25, A17, A20, A36, A47, A37, A51, A52, A56, A59, A65, A66, Th54, EUCLID:52, JGRAPH_4:82; :: 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 A67: 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 )
W-min P = |[(- 1),0]| by A1, Th29;
then A68: p2 `1 = - 1 by A67, EUCLID:52;
then ( p2 = f1 . p2 & p1 `1 <= p2 `1 ) by A1, A2, A6, A17, Th47, JGRAPH_4:82;
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, A2, A3, A5, A6, A14, A15, A17, A28, A20, A33, A36, A47, A37, A51, A52, A68, Th54, JGRAPH_4:82; :: 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 A69: 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 )
A70: now :: thesis: ( ( p3 <> p4 & (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P & (f1 . p3) `2 >= 0 & LE f1 . p3,f1 . p4,P ) or ( p3 = p4 & (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P & (f1 . p3) `2 >= 0 & LE f1 . p3,f1 . p4,P ) )
per cases ( p3 <> p4 or p3 = p4 ) ;
case A71: p3 <> p4 ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P & (f1 . p3) `2 >= 0 & LE f1 . p3,f1 . p4,P )
A72: now :: thesis: ( p2 `1 = 0 implies not p2 `2 = - 1 )
A73: LE p2,p4,P by A1, A3, A4, JGRAPH_3:26, JORDAN6:58;
assume that
A74: p2 `1 = 0 and
A75: p2 `2 = - 1 ; :: thesis: contradiction
p2 `2 <= p4 `2 by A11, A75, Th1;
then LE p4,p2,P by A1, A8, A29, A10, A33, A74, Th55;
hence contradiction by A1, A8, A74, A75, A73, JGRAPH_3:26, JORDAN6:57; :: thesis: verum
end;
p3 `2 > p4 `2 by A1, A4, A8, A33, A69, A71, Th50;
then A76: (p3 `2) / |.p3.| >= r1 by A26, A15, XXREAL_0:2;
then A77: (f1 . p3) `1 > 0 by A16, A17, A69, JGRAPH_4:106;
A78: (f1 . p3) `2 >= 0 by A16, A17, A69, A76, JGRAPH_4:106;
A79: now :: thesis: ( not p2 `1 = 0 or p2 `2 = 1 or p2 `2 = - 1 )
assume p2 `1 = 0 ; :: thesis: ( p2 `2 = 1 or p2 `2 = - 1 )
then 1 ^2 = (0 ^2) + ((p2 `2) ^2) by A30, JGRAPH_3:1;
hence ( p2 `2 = 1 or p2 `2 = - 1 ) by SQUARE_1:40; :: thesis: verum
end;
A80: now :: thesis: ( ( p2 `1 <= 0 & p2 `2 >= 0 & (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) or ( p2 `1 > 0 & (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) )
per cases ( ( p2 `1 <= 0 & p2 `2 >= 0 ) or p2 `1 > 0 ) by A6, A79, A72;
case A81: ( p2 `1 <= 0 & p2 `2 >= 0 ) ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )
then f1 . p2 = p2 by A17, JGRAPH_4:82;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) by A1, A29, A28, A77, A78, A81, Th54; :: thesis: verum
end;
case A82: p2 `1 > 0 ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )
then A83: (f1 . p2) `1 > 0 by A14, A16, A17, Th22;
now :: thesis: ( ( p2 = p3 & (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) or ( p2 <> p3 & (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) )
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 A9, A16, A17, A28, A69, A76, JGRAPH_4:106, JORDAN6:56; :: 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, A3, A30, A26, A69, A82, Th50;
then ((f1 . p2) `2) / |.(f1 . p2).| > ((f1 . p3) `2) / |.(f1 . p3).| by A30, A26, A14, A16, A17, A69, A82, Th24;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) by A1, A16, A17, A31, A32, A27, A28, A69, A76, A77, A83, Th55, JGRAPH_4:106; :: thesis: verum
end;
end;
end;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) ; :: thesis: verum
end;
end;
end;
(p3 `2) / |.p3.| > (p4 `2) / |.p4.| by A1, A4, A8, A11, A26, A33, A69, A71, Th50;
then ((f1 . p3) `2) / |.(f1 . p3).| > ((f1 . p4) `2) / |.(f1 . p4).| by A8, A11, A26, A14, A15, A17, A33, A69, Th24;
then ((f1 . p3) `2) ^2 > ((f1 . p4) `2) ^2 by A27, A19, A47, SQUARE_1:16;
then A84: (1 ^2) - (((f1 . p3) `2) ^2) < (1 ^2) - (((f1 . p4) `2) ^2) by XREAL_1:15;
1 ^2 = (((f1 . p4) `1) ^2) + (((f1 . p4) `2) ^2) by A19, JGRAPH_3:1;
then A85: (f1 . p4) `1 = sqrt ((1 ^2) - (((f1 . p4) `2) ^2)) by A36, SQUARE_1:22;
A86: 1 ^2 = (((f1 . p3) `1) ^2) + (((f1 . p3) `2) ^2) by A27, JGRAPH_3:1;
then (f1 . p3) `1 = sqrt ((1 ^2) - (((f1 . p3) `2) ^2)) by A77, SQUARE_1:22;
then (f1 . p3) `1 < (f1 . p4) `1 by A86, A85, A84, SQUARE_1:27, XREAL_1:63;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P & (f1 . p3) `2 >= 0 & LE f1 . p3,f1 . p4,P ) by A1, A28, A20, A47, A78, A80, Th54; :: thesis: verum
end;
case A87: p3 = p4 ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P & (f1 . p3) `2 >= 0 & LE f1 . p3,f1 . p4,P )
A88: now :: thesis: ( p2 `1 = 0 implies not p2 `2 = - 1 )
A89: LE p2,p4,P by A1, A3, A4, JGRAPH_3:26, JORDAN6:58;
assume A90: ( p2 `1 = 0 & p2 `2 = - 1 ) ; :: thesis: contradiction
then LE p4,p2,P by A1, A8, A29, A10, A12, A33, Th55;
hence contradiction by A1, A8, A90, A89, JGRAPH_3:26, JORDAN6:57; :: thesis: verum
end;
A91: now :: thesis: ( not p2 `1 = 0 or p2 `2 = 1 or p2 `2 = - 1 )
assume p2 `1 = 0 ; :: thesis: ( p2 `2 = 1 or p2 `2 = - 1 )
then 1 ^2 = (0 ^2) + ((p2 `2) ^2) by A30, JGRAPH_3:1;
hence ( p2 `2 = 1 or p2 `2 = - 1 ) by SQUARE_1:40; :: thesis: verum
end;
A92: (p3 `2) / |.p3.| >= r1 by A26, A15, A87;
then A93: (f1 . p3) `1 > 0 by A16, A17, A69, JGRAPH_4:106;
A94: (f1 . p3) `2 >= 0 by A16, A17, A69, A92, JGRAPH_4:106;
now :: thesis: ( ( p2 `1 <= 0 & p2 `2 >= 0 & (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) or ( p2 `1 > 0 & (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) )
per cases ( ( p2 `1 <= 0 & p2 `2 >= 0 ) or p2 `1 > 0 ) by A6, A91, A88;
case A95: ( p2 `1 <= 0 & p2 `2 >= 0 ) ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )
then f1 . p2 = p2 by A17, JGRAPH_4:82;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) by A1, A29, A28, A93, A94, A95, Th54; :: thesis: verum
end;
case A96: p2 `1 > 0 ; :: thesis: ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )
then A97: (f1 . p2) `1 > 0 by A14, A16, A17, Th22;
now :: thesis: ( ( p2 = p3 & (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) or ( p2 <> p3 & (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) )
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 A9, A16, A17, A28, A69, A92, JGRAPH_4:106, JORDAN6:56; :: 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, A3, A30, A26, A69, A96, Th50;
then ((f1 . p2) `2) / |.(f1 . p2).| > ((f1 . p3) `2) / |.(f1 . p3).| by A30, A26, A14, A16, A17, A69, A96, Th24;
hence ( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P ) by A1, A16, A17, A31, A32, A27, A28, A69, A92, A93, A97, Th55, JGRAPH_4:106; :: 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, A28, A36, A47, A87, Th54; :: thesis: verum
end;
end;
end;
A98: now :: thesis: ( p1 `1 = 0 implies not p1 `2 = - 1 )
LE p1,p3,P by A1, A2, A3, JGRAPH_3:26, JORDAN6:58;
then A99: LE p1,p4,P by A1, A4, JGRAPH_3:26, JORDAN6:58;
assume A100: ( p1 `1 = 0 & p1 `2 = - 1 ) ; :: thesis: contradiction
then LE p4,p1,P by A1, A8, A21, A10, A12, A33, Th55;
hence contradiction by A1, A8, A100, A99, JGRAPH_3:26, JORDAN6:57; :: thesis: verum
end;
A101: now :: thesis: ( not p2 `1 = 0 or p2 `2 = 1 or p2 `2 = - 1 )
assume p2 `1 = 0 ; :: thesis: ( p2 `2 = 1 or p2 `2 = - 1 )
then 1 ^2 = (0 ^2) + ((p2 `2) ^2) by A30, JGRAPH_3:1;
hence ( p2 `2 = 1 or p2 `2 = - 1 ) by SQUARE_1:40; :: thesis: verum
end;
A102: now :: thesis: ( p2 `1 = 0 implies not p2 `2 = - 1 )
A103: LE p2,p4,P by A1, A3, A4, JGRAPH_3:26, JORDAN6:58;
assume that
A104: p2 `1 = 0 and
A105: p2 `2 = - 1 ; :: thesis: contradiction
p2 `2 <= p4 `2 by A11, A105, Th1;
then LE p4,p2,P by A1, A8, A29, A10, A33, A104, Th55;
hence contradiction by A1, A8, A104, A105, A103, JGRAPH_3:26, JORDAN6:57; :: thesis: verum
end;
A106: now :: thesis: ( not p1 `1 = 0 or p1 `2 = 1 or p1 `2 = - 1 )
assume p1 `1 = 0 ; :: thesis: ( p1 `2 = 1 or p1 `2 = - 1 )
then 1 ^2 = (0 ^2) + ((p1 `2) ^2) by A22, JGRAPH_3:1;
hence ( p1 `2 = 1 or p1 `2 = - 1 ) by SQUARE_1:40; :: thesis: verum
end;
now :: thesis: ( ( p1 `1 <= 0 & p1 `2 >= 0 & (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) or ( p1 `1 > 0 & (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) )
per cases ( ( p1 `1 <= 0 & p1 `2 >= 0 ) or p1 `1 > 0 ) by A5, A106, A98;
case A107: ( p1 `1 <= 0 & p1 `2 >= 0 ) ; :: thesis: ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )
then A108: p1 = f1 . p1 by A17, JGRAPH_4:82;
A109: (f1 . p1) `2 >= 0 by A17, A107, JGRAPH_4:82;
now :: thesis: ( ( p2 `1 <= 0 & p2 `2 >= 0 & (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) or ( p2 `1 > 0 & (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) )
per cases ( ( p2 `1 <= 0 & p2 `2 >= 0 ) or p2 `1 > 0 ) by A6, A101, A102;
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 A2, A17, A107, A108, JGRAPH_4:82; :: 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 A14, A16, A17, A107, A108, Th22;
hence ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) by A1, A24, A32, A70, A109, Th54; :: thesis: verum
end;
end;
end;
hence ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) ; :: thesis: verum
end;
case A110: p1 `1 > 0 ; :: thesis: ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )
then A111: (f1 . p1) `1 > 0 by A14, A16, A17, Th22;
now :: thesis: ( ( p2 `1 <= 0 & p2 `2 >= 0 & (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) or ( p2 `1 > 0 & (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) )
per cases ( ( p2 `1 <= 0 & p2 `2 >= 0 ) or p2 `1 > 0 ) by A6, A101, A102;
case A112: ( p2 `1 <= 0 & p2 `2 >= 0 ) ; :: thesis: ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )
then LE p2,p1,P by A1, A21, A29, A110, A112, Th54;
then f1 . p1 = f1 . p2 by A1, A2, JGRAPH_3:26, JORDAN6:57;
hence ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) by A9, A17, A24, A112, JGRAPH_4:82, JORDAN6:56; :: thesis: verum
end;
case A116: p2 `1 > 0 ; :: thesis: ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )
then A117: (f1 . p2) `1 > 0 by A14, A16, A17, Th22;
now :: thesis: ( ( p1 = p2 & (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) or ( p1 <> p2 & (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) )
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, A24, A70, JGRAPH_3:26, JORDAN6:56; :: 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, A2, A22, A30, A110, A116, Th50;
then ((f1 . p1) `2) / |.(f1 . p1).| > ((f1 . p2) `2) / |.(f1 . p2).| by A22, A30, A14, A16, A17, A110, A116, Th24;
hence ( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P ) by A1, A23, A24, A31, A32, A70, A111, A117, Th55; :: 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 A8, A15, A17, A33, A35, A37, A70, JGRAPH_4:106; :: thesis: verum
end;
end;
end;
for q being Point of (TOP-REAL 2) holds |.(f1 . q).| = |.q.| by A17, JGRAPH_4:97;
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 A18, A49; :: thesis: verum
end;
case A118: 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 )
A119: Lower_Arc P = { p8 where p8 is Point of (TOP-REAL 2) : ( p8 in P & p8 `2 <= 0 ) } by A1, Th35;
A120: now :: thesis: not p4 in Lower_Arc P
assume p4 in Lower_Arc P ; :: thesis: contradiction
then ex p9 being Point of (TOP-REAL 2) st
( p9 = p4 & p9 in P & p9 `2 <= 0 ) by A119;
hence contradiction by A118; :: thesis: verum
end;
A121: Upper_Arc P = { p7 where p7 is Point of (TOP-REAL 2) : ( p7 in P & p7 `2 >= 0 ) } by A1, Th34;
( ( 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 A4;
then A122: ex p33 being Point of (TOP-REAL 2) st
( p33 = p3 & p33 in P & p33 `2 >= 0 ) by A121, A120;
set f4 = id (TOP-REAL 2);
A123: ( (id (TOP-REAL 2)) . p3 = p3 & (id (TOP-REAL 2)) . p4 = p4 ) ;
A124: for q being Point of (TOP-REAL 2) holds |.((id (TOP-REAL 2)) . q).| = |.q.| ;
A125: LE p2,p4,P by A1, A3, A4, JGRAPH_3:26, JORDAN6:58;
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 ) ) ;
then A126: ex p22 being Point of (TOP-REAL 2) st
( p22 = p2 & p22 in P & p22 `2 >= 0 ) by A121, A120;
LE p1,p4,P by A1, A2, A125, JGRAPH_3:26, JORDAN6:58;
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 ) ) ;
then A127: ex p11 being Point of (TOP-REAL 2) st
( p11 = p1 & p11 in P & p11 `2 >= 0 ) by A121, A120;
( (id (TOP-REAL 2)) . p1 = p1 & (id (TOP-REAL 2)) . p2 = p2 ) ;
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 A2, A3, A4, A118, A122, A126, A127, A123, A124; :: 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