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 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); ( 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 )
; 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;
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 ( ( 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
;
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 not (f1 . p4) `2 = 0 set q8 =
|[(sqrt (1 - (r1 ^2))),r1]|;
assume A38:
(f1 . p4) `2 = 0
;
contradiction1
^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
by SQUARE_1:18
;
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;
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 ( ( 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
;
( (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;
now ( ( 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
;
( (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:
now not p2 `2 < 0 A57:
p3 in Upper_Arc P
by A25, A34, A51, A52;
assume A58:
p2 `2 < 0
;
contradictionthen
p2 in Lower_Arc P
by A29, A48;
then
LE p3,
p2,
P
by A55, A57;
hence
contradiction
by A1, A3, A51, A52, A58, JGRAPH_3:26, JORDAN6:57;
verum end; A59:
p2 `1 <= p3 `1
by A1, A3, A51, A52, Th47;
then A60:
f1 . p2 = p2
by A17, A50, JGRAPH_4:82;
now ( ( 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
;
( (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 )A62:
now not p1 `2 < 0 A63:
p2 in Upper_Arc P
by A29, A34, A56;
assume A64:
p1 `2 < 0
;
contradictionthen
p1 in Lower_Arc P
by A21, A48;
then
LE p2,
p1,
P
by A61, A63;
hence
contradiction
by A1, A2, A56, A64, JGRAPH_3:26, JORDAN6:57;
verum end;
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;
verum end; case A65:
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 )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;
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 )
;
verum end; case A67:
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 )
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;
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 )
;
verum end; case A69:
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 )A70:
now ( ( 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
;
( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P & (f1 . p3) `2 >= 0 & LE f1 . p3,f1 . p4,P )A72:
now ( 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
;
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;
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;
A80:
now ( ( 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 A82:
p2 `1 > 0
;
( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )then A83:
(f1 . p2) `1 > 0
by A14, A16, A17, Th22;
now ( ( 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
;
( (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;
verum end; end; end; hence
(
(f1 . p2) `2 >= 0 &
LE f1 . p2,
f1 . p3,
P )
;
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;
verum end; case A87:
p3 = p4
;
( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P & (f1 . p3) `2 >= 0 & LE f1 . p3,f1 . p4,P )A88:
now ( 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 )
;
contradictionthen
LE p4,
p2,
P
by A1, A8, A29, A10, A12, A33, Th55;
hence
contradiction
by A1, A8, A90, A89, JGRAPH_3:26, JORDAN6:57;
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 ( ( 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 A96:
p2 `1 > 0
;
( (f1 . p2) `2 >= 0 & LE f1 . p2,f1 . p3,P )then A97:
(f1 . p2) `1 > 0
by A14, A16, A17, Th22;
now ( ( 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
;
( (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;
verum end; end; end; hence
(
(f1 . p2) `2 >= 0 &
LE f1 . p2,
f1 . p3,
P )
;
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;
verum end; end; end; A98:
now ( 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 )
;
contradictionthen
LE p4,
p1,
P
by A1, A8, A21, A10, A12, A33, Th55;
hence
contradiction
by A1, A8, A100, A99, JGRAPH_3:26, JORDAN6:57;
verum end; A102:
now ( 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
;
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;
verum end; now ( ( 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 )
;
( (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 ( ( 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
;
( (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;
verum end; end; end; hence
(
(f1 . p1) `2 >= 0 &
LE f1 . p1,
f1 . p2,
P )
;
verum end; case A110:
p1 `1 > 0
;
( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )then A111:
(f1 . p1) `1 > 0
by A14, A16, A17, Th22;
now ( ( 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 )
;
( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )now not p1 `2 < 0 A113:
p2 in Upper_Arc P
by A29, A34, A112;
assume A114:
p1 `2 < 0
;
contradiction
W-min P = |[(- 1),0]|
by A1, Th29;
then A115:
p1 <> W-min P
by A114, EUCLID:52;
p1 in Lower_Arc P
by A21, A48, A114;
then
LE p2,
p1,
P
by A113, A115;
hence
contradiction
by A1, A2, A110, A112, JGRAPH_3:26, JORDAN6:57;
verum end; 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;
verum end; case A116:
p2 `1 > 0
;
( (f1 . p1) `2 >= 0 & LE f1 . p1,f1 . p2,P )then A117:
(f1 . p2) `1 > 0
by A14, A16, A17, Th22;
now ( ( 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
;
( (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;
verum end; end; end; hence
(
(f1 . p1) `2 >= 0 &
LE f1 . p1,
f1 . p2,
P )
;
verum end; end; end; hence
(
(f1 . p1) `2 >= 0 &
LE f1 . p1,
f1 . p2,
P )
;
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;
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;
verum end; case A118:
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 )A119:
Lower_Arc P = { p8 where p8 is Point of (TOP-REAL 2) : ( p8 in P & p8 `2 <= 0 ) }
by A1, Th35;
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;
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 )
; verum