let cn be Real; for p1, p2, q1, q2 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2) st - 1 < cn & cn < 1 & P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & q1 = (cn -FanMorphS) . p1 & q2 = (cn -FanMorphS) . p2 holds
LE q1,q2,P
let p1, p2, q1, q2 be Point of (TOP-REAL 2); for P being non empty compact Subset of (TOP-REAL 2) st - 1 < cn & cn < 1 & P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & q1 = (cn -FanMorphS) . p1 & q2 = (cn -FanMorphS) . p2 holds
LE q1,q2,P
let P be non empty compact Subset of (TOP-REAL 2); ( - 1 < cn & cn < 1 & P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & q1 = (cn -FanMorphS) . p1 & q2 = (cn -FanMorphS) . p2 implies LE q1,q2,P )
assume that
A1:
( - 1 < cn & cn < 1 )
and
A2:
P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 }
and
A3:
LE p1,p2,P
and
A4:
q1 = (cn -FanMorphS) . p1
and
A5:
q2 = (cn -FanMorphS) . p2
; LE q1,q2,P
A6:
P is being_simple_closed_curve
by A2, JGRAPH_3:26;
W-min P = |[(- 1),0]|
by A2, Th29;
then A7:
(W-min P) `2 = 0
by EUCLID:52;
then A8:
(cn -FanMorphS) . (W-min P) = W-min P
by JGRAPH_4:113;
p2 in the carrier of (TOP-REAL 2)
;
then A9:
p2 in dom (cn -FanMorphS)
by FUNCT_2:def 1;
W-min P in the carrier of (TOP-REAL 2)
;
then A10:
W-min P in dom (cn -FanMorphS)
by FUNCT_2:def 1;
A11:
Lower_Arc P c= P
by A2, Th33;
A12:
cn -FanMorphS is one-to-one
by A1, JGRAPH_4:133;
A13:
Upper_Arc P c= P
by A2, Th33;
A15:
now ( not q2 = W-min P or ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) )assume A16:
q2 = W-min P
;
( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) )then
p2 = W-min P
by A5, A8, A10, A9, A12, FUNCT_1:def 4;
then
LE p2,
p1,
P
by A6, A14, JORDAN7:3;
then A17:
q1 = q2
by A2, A3, A4, A5, JGRAPH_3:26, JORDAN6:57;
W-min P in Lower_Arc P
by A6, JORDAN7:1;
then
LE q1,
q2,
P
by A2, A11, A16, A17, JGRAPH_3:26, JORDAN6:56;
hence
( (
q1 in Upper_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P ) or (
q1 in Upper_Arc P &
q2 in Upper_Arc P &
LE q1,
q2,
Upper_Arc P,
W-min P,
E-max P ) or (
q1 in Lower_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P &
LE q1,
q2,
Lower_Arc P,
E-max P,
W-min P ) )
;
verum end;
A18:
Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
by A2, Th34;
A19:
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) }
by A2, Th35;
per cases
( ( p1 in Upper_Arc P & p2 in Lower_Arc P & not p2 = W-min P ) or ( p1 in Upper_Arc P & p2 in Upper_Arc P & LE p1,p2, Upper_Arc P, W-min P, E-max P ) or ( p1 in Lower_Arc P & p2 in Lower_Arc P & not p2 = W-min P & LE p1,p2, Lower_Arc P, E-max P, W-min P & not p1 in Upper_Arc P ) )
by A3;
suppose A20:
(
p1 in Upper_Arc P &
p2 in Lower_Arc P & not
p2 = W-min P )
;
LE q1,q2,PA21:
|.q2.| = |.p2.|
by A5, JGRAPH_4:128;
A22:
ex
p9 being
Point of
(TOP-REAL 2) st
(
p9 = p2 &
p9 in P &
p9 `2 <= 0 )
by A19, A20;
then
ex
p10 being
Point of
(TOP-REAL 2) st
(
p10 = p2 &
|.p10.| = 1 )
by A2;
then A23:
q2 in P
by A2, A21;
A24:
ex
p8 being
Point of
(TOP-REAL 2) st
(
p8 = p1 &
p8 in P &
p8 `2 >= 0 )
by A18, A20;
q2 `2 <= 0
by A1, A5, A22, Th57;
hence
( (
q1 in Upper_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P ) or (
q1 in Upper_Arc P &
q2 in Upper_Arc P &
LE q1,
q2,
Upper_Arc P,
W-min P,
E-max P ) or (
q1 in Lower_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P &
LE q1,
q2,
Lower_Arc P,
E-max P,
W-min P ) )
by A4, A19, A15, A20, A24, A23, JGRAPH_4:113;
JORDAN6:def 10 verum end; suppose A25:
(
p1 in Upper_Arc P &
p2 in Upper_Arc P &
LE p1,
p2,
Upper_Arc P,
W-min P,
E-max P )
;
LE q1,q2,Pthen
ex
p8 being
Point of
(TOP-REAL 2) st
(
p8 = p1 &
p8 in P &
p8 `2 >= 0 )
by A18;
then A26:
p1 = (cn -FanMorphS) . p1
by JGRAPH_4:113;
ex
p9 being
Point of
(TOP-REAL 2) st
(
p9 = p2 &
p9 in P &
p9 `2 >= 0 )
by A18, A25;
hence
( (
q1 in Upper_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P ) or (
q1 in Upper_Arc P &
q2 in Upper_Arc P &
LE q1,
q2,
Upper_Arc P,
W-min P,
E-max P ) or (
q1 in Lower_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P &
LE q1,
q2,
Lower_Arc P,
E-max P,
W-min P ) )
by A4, A5, A25, A26, JGRAPH_4:113;
JORDAN6:def 10 verum end; suppose A27:
(
p1 in Lower_Arc P &
p2 in Lower_Arc P & not
p2 = W-min P &
LE p1,
p2,
Lower_Arc P,
E-max P,
W-min P & not
p1 in Upper_Arc P )
;
LE q1,q2,Pthen A28:
ex
p8 being
Point of
(TOP-REAL 2) st
(
p8 = p1 &
p8 in P &
p8 `2 <= 0 )
by A19;
then A29:
ex
p10 being
Point of
(TOP-REAL 2) st
(
p10 = p1 &
|.p10.| = 1 )
by A2;
A30:
ex
p9 being
Point of
(TOP-REAL 2) st
(
p9 = p2 &
p9 in P &
p9 `2 <= 0 )
by A19, A27;
then A31:
ex
p11 being
Point of
(TOP-REAL 2) st
(
p11 = p2 &
|.p11.| = 1 )
by A2;
A32:
q2 `2 <= 0
by A1, A5, A30, Th57;
A33:
|.q2.| = |.p2.|
by A5, JGRAPH_4:128;
then A34:
q2 in P
by A2, A31;
A35:
q1 `2 <= 0
by A1, A4, A28, Th57;
A36:
|.q1.| = |.p1.|
by A4, JGRAPH_4:128;
then A37:
q1 in P
by A2, A29;
now ( ( p1 = W-min P & ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) ) or ( p1 <> W-min P & ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) ) )per cases
( p1 = W-min P or p1 <> W-min P )
;
case A38:
p1 = W-min P
;
( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) )then
p1 = (cn -FanMorphS) . p1
by A7, JGRAPH_4:113;
then
LE q1,
q2,
P
by A4, A6, A34, A38, JORDAN7:3;
hence
( (
q1 in Upper_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P ) or (
q1 in Upper_Arc P &
q2 in Upper_Arc P &
LE q1,
q2,
Upper_Arc P,
W-min P,
E-max P ) or (
q1 in Lower_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P &
LE q1,
q2,
Lower_Arc P,
E-max P,
W-min P ) )
;
verum end; case A39:
p1 <> W-min P
;
( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) )now ( ( p1 `1 = p2 `1 & ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) ) or ( p1 `1 > p2 `1 & ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) ) )per cases
( p1 `1 = p2 `1 or p1 `1 > p2 `1 )
by A2, A3, A28, A39, Th48;
case A40:
p1 `1 = p2 `1
;
( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) )A41:
p2 = |[(p2 `1),(p2 `2)]|
by EUCLID:53;
A42:
now ( p1 `2 = - (p2 `2) implies p1 = p2 )end; ((p1 `1) ^2) + ((p1 `2) ^2) =
1
^2
by A29, JGRAPH_3:1
.=
((p1 `1) ^2) + ((p2 `2) ^2)
by A31, A40, JGRAPH_3:1
;
then A44:
(
p1 `2 = p2 `2 or
p1 `2 = - (p2 `2) )
by SQUARE_1:40;
p1 = |[(p1 `1),(p1 `2)]|
by EUCLID:53;
then
LE q1,
q2,
P
by A2, A4, A5, A34, A40, A44, A41, A42, JGRAPH_3:26, JORDAN6:56;
hence
( (
q1 in Upper_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P ) or (
q1 in Upper_Arc P &
q2 in Upper_Arc P &
LE q1,
q2,
Upper_Arc P,
W-min P,
E-max P ) or (
q1 in Lower_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P &
LE q1,
q2,
Lower_Arc P,
E-max P,
W-min P ) )
;
verum end; case
p1 `1 > p2 `1
;
( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) )then
(p1 `1) / |.p1.| > (p2 `1) / |.p2.|
by A29, A31;
then A45:
(q1 `1) / |.q1.| >= (q2 `1) / |.q2.|
by A1, A4, A5, A28, A30, A29, A31, Th27;
q2 <> W-min P
by A5, A8, A10, A9, A12, A27, FUNCT_1:def 4;
then
LE q1,
q2,
P
by A2, A36, A33, A35, A32, A29, A31, A37, A34, A45, Th56;
hence
( (
q1 in Upper_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P ) or (
q1 in Upper_Arc P &
q2 in Upper_Arc P &
LE q1,
q2,
Upper_Arc P,
W-min P,
E-max P ) or (
q1 in Lower_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P &
LE q1,
q2,
Lower_Arc P,
E-max P,
W-min P ) )
;
verum end; end; end; hence
( (
q1 in Upper_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P ) or (
q1 in Upper_Arc P &
q2 in Upper_Arc P &
LE q1,
q2,
Upper_Arc P,
W-min P,
E-max P ) or (
q1 in Lower_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P &
LE q1,
q2,
Lower_Arc P,
E-max P,
W-min P ) )
;
verum end; end; end; hence
( (
q1 in Upper_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P ) or (
q1 in Upper_Arc P &
q2 in Upper_Arc P &
LE q1,
q2,
Upper_Arc P,
W-min P,
E-max P ) or (
q1 in Lower_Arc P &
q2 in Lower_Arc P & not
q2 = W-min P &
LE q1,
q2,
Lower_Arc P,
E-max P,
W-min P ) )
;
JORDAN6:def 10 verum end; end;