:: General {F}ashoda {M}eet {T}heorem for Unit Circle
:: by Yatsuka Nakamura
::
:: Received June 24, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users

theorem Th1: :: JGRAPH_5:1

for p being Point of (TOP-REAL 2) st |.p.| <= 1 holds
( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 )

proof end;

theorem Th2: :: JGRAPH_5:2

for p being Point of (TOP-REAL 2) st |.p.| <= 1 & p `1 <> 0 & p `2 <> 0 holds
( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 )

proof end;

theorem :: JGRAPH_5:3

for a, b, d, e, r3 being Real
for PM, PM2 being non empty MetrStruct
for x being Element of PM
for x2 being Element of PM2 st d <= a & a <= b & b <= e & PM = Closed-Interval-MSpace (a,b) & PM2 = Closed-Interval-MSpace (d,e) & x = x2 holds
Ball (x,r3) c= Ball (x2,r3)

proof end;

theorem :: JGRAPH_5:4

for a, b being Real
for B being Subset of I[01] st 0 <= a & a <= b & b <= 1 & B = [.a,b.] holds
Closed-Interval-TSpace (a,b) = I[01] | B by TOPMETR:20, TOPMETR:23;

theorem Th5: :: JGRAPH_5:5

for X being TopStruct
for Y, Z being non empty TopStruct
for f being Function of X,Y
for h being Function of Y,Z st h is being_homeomorphism & f is continuous holds
h * f is continuous

proof end;

theorem Th6: :: JGRAPH_5:6

for X, Y, Z being TopStruct
for f being Function of X,Y
for h being Function of Y,Z st h is being_homeomorphism & f is one-to-one holds
h * f is one-to-one

proof end;

theorem Th7: :: JGRAPH_5:7

for X being TopStruct
for S, V being non empty TopStruct
for B being non empty Subset of S
for f being Function of X,(S | B)
for g being Function of S,V
for h being Function of X,V st h = g * f & f is continuous & g is continuous holds
h is continuous

proof end;

theorem Th8: :: JGRAPH_5:8

for a, b, d, e, s1, s2, t1, t2 being Real
for h being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (d,e)) st h is being_homeomorphism & h . s1 = t1 & h . s2 = t2 & h . b = e & d <= e & t1 <= t2 & s1 in [.a,b.] & s2 in [.a,b.] holds
s1 <= s2

proof end;

theorem Th9: :: JGRAPH_5:9

for a, b, d, e, s1, s2, t1, t2 being Real
for h being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (d,e)) st h is being_homeomorphism & h . s1 = t1 & h . s2 = t2 & h . b = d & e >= d & t1 >= t2 & s1 in [.a,b.] & s2 in [.a,b.] holds
s1 <= s2

proof end;

theorem :: JGRAPH_5:10

for n being Element of NAT holds - (0. (TOP-REAL n)) = 0. (TOP-REAL n)

proof end;

theorem Th11: :: JGRAPH_5:11

for f, g being Function of I[01],(TOP-REAL 2)
for a, b, c, d being Real
for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & a <> b & c <> d & (f . O) `1 = a & c <= (f . O) `2 & (f . O) `2 <= d & (f . I) `1 = b & c <= (f . I) `2 & (f . I) `2 <= d & (g . O) `2 = c & a <= (g . O) `1 & (g . O) `1 <= b & (g . I) `2 = d & a <= (g . I) `1 & (g . I) `1 <= b & ( for r being Point of I[01] holds
( ( a >= (f . r) `1 or (f . r) `1 >= b or c >= (f . r) `2 or (f . r) `2 >= d ) & ( a >= (g . r) `1 or (g . r) `1 >= b or c >= (g . r) `2 or (g . r) `2 >= d ) ) ) holds
rng f meets rng g

proof end;

Lm1: 0 in [.0,1.]
by XXREAL_1:1;

Lm2: 1 in [.0,1.]
by XXREAL_1:1;

theorem Th12: :: JGRAPH_5:12

for f being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one holds
ex f2 being Function of I[01],(TOP-REAL 2) st
( f2 . 0 = f . 1 & f2 . 1 = f . 0 & rng f2 = rng f & f2 is continuous & f2 is one-to-one )

proof end;

theorem Th13: :: JGRAPH_5:13

for f, g being Function of I[01],(TOP-REAL 2)
for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)
for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1) ) } & f . O in KXN & f . I in KXP & g . O in KYP & g . I in KYN & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

proof end;

theorem Th14: :: JGRAPH_5:14

for f, g being Function of I[01],(TOP-REAL 2)
for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)
for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1) ) } & f . O in KXN & f . I in KXP & g . O in KYN & g . I in KYP & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

proof end;

theorem Th15: :: JGRAPH_5:15

for f, g being Function of I[01],(TOP-REAL 2)
for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)
for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1) ) } & f . O in KXN & f . I in KXP & g . O in KYP & g . I in KYN & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

proof end;

theorem Th16: :: JGRAPH_5:16

for f, g being Function of I[01],(TOP-REAL 2)
for C0 being Subset of (TOP-REAL 2) st C0 = { q where q is Point of (TOP-REAL 2) : |.q.| >= 1 } & f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = |[(- 1),0]| & f . 1 = |[1,0]| & g . 1 = |[0,1]| & g . 0 = |[0,(- 1)]| & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

proof end;

theorem :: JGRAPH_5:17

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for C0 being Subset of (TOP-REAL 2) st C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & |.p1.| = 1 & |.p2.| = 1 & |.p3.| = 1 & |.p4.| = 1 & ex h being Function of (TOP-REAL 2),(TOP-REAL 2) st
( h is being_homeomorphism & h .: C0 c= C0 & h . p1 = |[(- 1),0]| & h . p2 = |[0,1]| & h . p3 = |[1,0]| & h . p4 = |[0,(- 1)]| ) holds
for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

proof end;

theorem Th18: :: JGRAPH_5:18

for cn being Real
for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 > 0 holds
for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds
p `2 > 0

proof end;

theorem :: JGRAPH_5:19

for cn being Real
for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 >= 0 holds
for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds
p `2 >= 0

proof end;

theorem Th20: :: JGRAPH_5:20

for cn being Real
for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 >= 0 & (q `1) / |.q.| < cn & |.q.| <> 0 holds
for p being Point of (TOP-REAL 2) st p = (cn -FanMorphN) . q holds
( p `2 >= 0 & p `1 < 0 )

proof end;

theorem Th21: :: JGRAPH_5:21

for cn being Real
for q1, q2 being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q1 `2 >= 0 & q2 `2 >= 0 & |.q1.| <> 0 & |.q2.| <> 0 & (q1 `1) / |.q1.| < (q2 `1) / |.q2.| holds
for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphN) . q1 & p2 = (cn -FanMorphN) . q2 holds
(p1 `1) / |.p1.| < (p2 `1) / |.p2.|

proof end;

theorem Th22: :: JGRAPH_5:22

for sn being Real
for q being Point of (TOP-REAL 2) st - 1 < sn & sn < 1 & q `1 > 0 holds
for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE) . q holds
p `1 > 0

proof end;

theorem :: JGRAPH_5:23

for sn being Real
for q being Point of (TOP-REAL 2) st - 1 < sn & sn < 1 & q `1 >= 0 & (q `2) / |.q.| < sn & |.q.| <> 0 holds
for p being Point of (TOP-REAL 2) st p = (sn -FanMorphE) . q holds
( p `1 >= 0 & p `2 < 0 )

proof end;

theorem Th24: :: JGRAPH_5:24

for sn being Real
for q1, q2 being Point of (TOP-REAL 2) st - 1 < sn & sn < 1 & q1 `1 >= 0 & q2 `1 >= 0 & |.q1.| <> 0 & |.q2.| <> 0 & (q1 `2) / |.q1.| < (q2 `2) / |.q2.| holds
for p1, p2 being Point of (TOP-REAL 2) st p1 = (sn -FanMorphE) . q1 & p2 = (sn -FanMorphE) . q2 holds
(p1 `2) / |.p1.| < (p2 `2) / |.p2.|

proof end;

theorem Th25: :: JGRAPH_5:25

for cn being Real
for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 < 0 holds
for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds
p `2 < 0

proof end;

theorem Th26: :: JGRAPH_5:26

for cn being Real
for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 < 0 & (q `1) / |.q.| > cn holds
for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds
( p `2 < 0 & p `1 > 0 )

proof end;

theorem Th27: :: JGRAPH_5:27

for cn being Real
for q1, q2 being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q1 `2 <= 0 & q2 `2 <= 0 & |.q1.| <> 0 & |.q2.| <> 0 & (q1 `1) / |.q1.| < (q2 `1) / |.q2.| holds
for p1, p2 being Point of (TOP-REAL 2) st p1 = (cn -FanMorphS) . q1 & p2 = (cn -FanMorphS) . q2 holds
(p1 `1) / |.p1.| < (p2 `1) / |.p2.|

proof end;

Lm3: now :: thesis: for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds
( proj1 .: P = [.(- 1),1.] & proj2 .: P = [.(- 1),1.] )

let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } implies ( proj1 .: P = [.(- 1),1.] & proj2 .: P = [.(- 1),1.] ) )
assume A1: P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } ; :: thesis: ( proj1 .: P = [.(- 1),1.] & proj2 .: P = [.(- 1),1.] )
A2: [.(- 1),1.] c= proj1 .: P

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [.(- 1),1.] or y in proj1 .: P )
assume y in [.(- 1),1.] ; :: thesis: y in proj1 .: P
then y in { r where r is Real : ( - 1 <= r & r <= 1 ) } by RCOMP_1:def 1;
then consider r being Real such that
A3: y = r and
A4: ( - 1 <= r & r <= 1 ) ;
set q = |[r,(sqrt (1 - (r ^2)))]|;
1 ^2 >= r ^2 by A4, SQUARE_1:49;
then A5: 1 - (r ^2) >= 0 by XREAL_1:48;
( |[r,(sqrt (1 - (r ^2)))]| `1 = r & |[r,(sqrt (1 - (r ^2)))]| `2 = sqrt (1 - (r ^2)) ) by EUCLID:52;
then |.|[r,(sqrt (1 - (r ^2)))]|.| = sqrt ((r ^2) + ((sqrt (1 - (r ^2))) ^2)) by JGRAPH_3:1
.= sqrt ((r ^2) + (1 - (r ^2))) by A5, SQUARE_1:def 2
.= 1 by SQUARE_1:18 ;
then A6: ( dom proj1 = the carrier of (TOP-REAL 2) & |[r,(sqrt (1 - (r ^2)))]| in P ) by A1, FUNCT_2:def 1;
proj1 . |[r,(sqrt (1 - (r ^2)))]| = |[r,(sqrt (1 - (r ^2)))]| `1 by PSCOMP_1:def 5
.= r by EUCLID:52 ;
hence y in proj1 .: P by A3, A6, FUNCT_1:def 6; :: thesis: verum

end;

proj1 .: P c= [.(- 1),1.]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in proj1 .: P or y in [.(- 1),1.] )
assume y in proj1 .: P ; :: thesis: y in [.(- 1),1.]
then consider x being object such that
A7: x in dom proj1 and
A8: x in P and
A9: y = proj1 . x by FUNCT_1:def 6;
reconsider q = x as Point of (TOP-REAL 2) by A7;
ex q2 being Point of (TOP-REAL 2) st
( q2 = x & |.q2.| = 1 ) by A1, A8;
then A10: ((q `1) ^2) + ((q `2) ^2) = 1 ^2 by JGRAPH_3:1;
0 <= (q `2) ^2 by XREAL_1:63;
then (1 - ((q `1) ^2)) + ((q `1) ^2) >= 0 + ((q `1) ^2) by A10, XREAL_1:7;
then A11: ( - 1 <= q `1 & q `1 <= 1 ) by SQUARE_1:51;
y = q `1 by A9, PSCOMP_1:def 5;
hence y in [.(- 1),1.] by A11, XXREAL_1:1; :: thesis: verum

end;

hence proj1 .: P = [.(- 1),1.] by A2, XBOOLE_0:def 10; :: thesis: proj2 .: P = [.(- 1),1.]
A12: [.(- 1),1.] c= proj2 .: P

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [.(- 1),1.] or y in proj2 .: P )
assume y in [.(- 1),1.] ; :: thesis: y in proj2 .: P
then y in { r where r is Real : ( - 1 <= r & r <= 1 ) } by RCOMP_1:def 1;
then consider r being Real such that
A13: y = r and
A14: ( - 1 <= r & r <= 1 ) ;
set q = |[(sqrt (1 - (r ^2))),r]|;
1 ^2 >= r ^2 by A14, SQUARE_1:49;
then A15: 1 - (r ^2) >= 0 by XREAL_1:48;
( |[(sqrt (1 - (r ^2))),r]| `2 = r & |[(sqrt (1 - (r ^2))),r]| `1 = sqrt (1 - (r ^2)) ) by EUCLID:52;
then |.|[(sqrt (1 - (r ^2))),r]|.| = sqrt (((sqrt (1 - (r ^2))) ^2) + (r ^2)) by JGRAPH_3:1
.= sqrt ((1 - (r ^2)) + (r ^2)) by A15, SQUARE_1:def 2
.= 1 by SQUARE_1:18 ;
then A16: ( dom proj2 = the carrier of (TOP-REAL 2) & |[(sqrt (1 - (r ^2))),r]| in P ) by A1, FUNCT_2:def 1;
proj2 . |[(sqrt (1 - (r ^2))),r]| = |[(sqrt (1 - (r ^2))),r]| `2 by PSCOMP_1:def 6
.= r by EUCLID:52 ;
hence y in proj2 .: P by A13, A16, FUNCT_1:def 6; :: thesis: verum

end;

proj2 .: P c= [.(- 1),1.]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in proj2 .: P or y in [.(- 1),1.] )
assume y in proj2 .: P ; :: thesis: y in [.(- 1),1.]
then consider x being object such that
A17: x in dom proj2 and
A18: x in P and
A19: y = proj2 . x by FUNCT_1:def 6;
reconsider q = x as Point of (TOP-REAL 2) by A17;
ex q2 being Point of (TOP-REAL 2) st
( q2 = x & |.q2.| = 1 ) by A1, A18;
then A20: ((q `1) ^2) + ((q `2) ^2) = 1 ^2 by JGRAPH_3:1;
0 <= (q `1) ^2 by XREAL_1:63;
then (1 - ((q `2) ^2)) + ((q `2) ^2) >= 0 + ((q `2) ^2) by A20, XREAL_1:7;
then A21: ( - 1 <= q `2 & q `2 <= 1 ) by SQUARE_1:51;
y = q `2 by A19, PSCOMP_1:def 6;
hence y in [.(- 1),1.] by A21, XXREAL_1:1; :: thesis: verum

end;

hence proj2 .: P = [.(- 1),1.] by A12, XBOOLE_0:def 10; :: thesis: verum

end;

Lm4: for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds
W-bound P = - 1

proof end;

theorem Th28: :: JGRAPH_5:28

for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds
( W-bound P = - 1 & E-bound P = 1 & S-bound P = - 1 & N-bound P = 1 )

proof end;

theorem Th29: :: JGRAPH_5:29

for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds
W-min P = |[(- 1),0]|

proof end;

theorem Th30: :: JGRAPH_5:30

for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds
E-max P = |[1,0]|

proof end;

theorem :: JGRAPH_5:31

for f being Function of (TOP-REAL 2),R^1 st ( for p being Point of (TOP-REAL 2) holds f . p = proj1 . p ) holds
f is continuous

proof end;

theorem Th32: :: JGRAPH_5:32

for f being Function of (TOP-REAL 2),R^1 st ( for p being Point of (TOP-REAL 2) holds f . p = proj2 . p ) holds
f is continuous

proof end;

theorem Th33: :: JGRAPH_5:33

for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds
( Upper_Arc P c= P & Lower_Arc P c= P )

proof end;

theorem Th34: :: JGRAPH_5:34

for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds
Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }

proof end;

theorem Th35: :: JGRAPH_5:35

for P being non empty compact Subset of (TOP-REAL 2) st P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } holds
Lower_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) }

proof end;

theorem Th36: :: JGRAPH_5:36

for a, b, d, e being Real st a <= b & e > 0 holds
ex f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * a) + d),((e * b) + d))) st
( f is being_homeomorphism & ( for r being Real st r in [.a,b.] holds
f . r = (e * r) + d ) )

proof end;

theorem Th37: :: JGRAPH_5:37

for a, b, d, e being Real st a <= b & e < 0 holds
ex f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (((e * b) + d),((e * a) + d))) st
( f is being_homeomorphism & ( for r being Real st r in [.a,b.] holds
f . r = (e * r) + d ) )

proof end;

theorem Th38: :: JGRAPH_5:38

ex f being Function of I[01],(Closed-Interval-TSpace ((- 1),1)) st
( f is being_homeomorphism & ( for r being Real st r in [.0,1.] holds
f . r = ((- 2) * r) + 1 ) & f . 0 = 1 & f . 1 = - 1 )

proof end;

theorem Th39: :: JGRAPH_5:39

ex f being Function of I[01],(Closed-Interval-TSpace ((- 1),1)) st
( f is being_homeomorphism & ( for r being Real st r in [.0,1.] holds
f . r = (2 * r) - 1 ) & f . 0 = - 1 & f . 1 = 1 )

proof end;

Lm5: now :: 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 } holds
( proj1 | (Lower_Arc P) is continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Lower_Arc P) is one-to-one & rng (proj1 | (Lower_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) )

reconsider B = [.(- 1),1.] as non empty Subset of R^1 by TOPMETR:17, XXREAL_1:1;
reconsider g = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } implies ( proj1 | (Lower_Arc P) is continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Lower_Arc P) is one-to-one & rng (proj1 | (Lower_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) ) )
set K0 = Lower_Arc P;
reconsider g2 = g | (Lower_Arc P) as Function of ((TOP-REAL 2) | (Lower_Arc P)),R^1 by PRE_TOPC:9;
A1: for p being Point of ((TOP-REAL 2) | (Lower_Arc P)) holds g2 . p = proj1 . p

proof

let p be Point of ((TOP-REAL 2) | (Lower_Arc P)); :: thesis: g2 . p = proj1 . p
p in the carrier of ((TOP-REAL 2) | (Lower_Arc P)) ;
then p in Lower_Arc P by PRE_TOPC:8;
hence g2 . p = proj1 . p by FUNCT_1:49; :: thesis: verum

end;

assume A2: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } ; :: thesis: ( proj1 | (Lower_Arc P) is continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Lower_Arc P) is one-to-one & rng (proj1 | (Lower_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) )
then A3: Lower_Arc P c= P by Th33;
A4: dom g2 = the carrier of ((TOP-REAL 2) | (Lower_Arc P)) by FUNCT_2:def 1;
then A5: dom g2 = Lower_Arc P by PRE_TOPC:8;
rng g2 c= the carrier of (Closed-Interval-TSpace ((- 1),1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g2 or x in the carrier of (Closed-Interval-TSpace ((- 1),1)) )
assume x in rng g2 ; :: thesis: x in the carrier of (Closed-Interval-TSpace ((- 1),1))
then consider z being object such that
A6: z in dom g2 and
A7: x = g2 . z by FUNCT_1:def 3;
z in P by A5, A3, A6;
then consider p being Point of (TOP-REAL 2) such that
A8: p = z and
A9: |.p.| = 1 by A2;
1 ^2 = ((p `1) ^2) + ((p `2) ^2) by A9, JGRAPH_3:1;
then 1 - ((p `1) ^2) >= 0 by XREAL_1:63;
then - (1 - ((p `1) ^2)) <= 0 ;
then ((p `1) ^2) - 1 <= 0 ;
then A10: ( - 1 <= p `1 & p `1 <= 1 ) by SQUARE_1:43;
x = proj1 . p by A1, A6, A7, A8
.= p `1 by PSCOMP_1:def 5 ;
then x in [.(- 1),1.] by A10, XXREAL_1:1;
hence x in the carrier of (Closed-Interval-TSpace ((- 1),1)) by TOPMETR:18; :: thesis: verum

end;

then reconsider g3 = g2 as Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) by A4, FUNCT_2:2;
dom g3 = [#] ((TOP-REAL 2) | (Lower_Arc P)) by FUNCT_2:def 1;
then A11: dom g3 = Lower_Arc P by PRE_TOPC:def 5;
A12: for x, y being object st x in dom g3 & y in dom g3 & g3 . x = g3 . y holds
x = y

proof

let x, y be object ; :: thesis: ( x in dom g3 & y in dom g3 & g3 . x = g3 . y implies x = y )
assume that
A13: x in dom g3 and
A14: y in dom g3 and
A15: g3 . x = g3 . y ; :: thesis: x = y
reconsider p2 = y as Point of (TOP-REAL 2) by A11, A14;
A16: g3 . y = proj1 . p2 by A1, A14
.= p2 `1 by PSCOMP_1:def 5 ;
reconsider p1 = x as Point of (TOP-REAL 2) by A11, A13;
A17: g3 . x = proj1 . p1 by A1, A13
.= p1 `1 by PSCOMP_1:def 5 ;
p2 in P by A3, A11, A14;
then ex p22 being Point of (TOP-REAL 2) st
( p2 = p22 & |.p22.| = 1 ) by A2;
then A18: 1 ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;
p2 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 <= 0 ) } by A2, A11, A14, Th35;
then A19: ex p44 being Point of (TOP-REAL 2) st
( p2 = p44 & p44 in P & p44 `2 <= 0 ) ;
p1 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 <= 0 ) } by A2, A11, A13, Th35;
then A20: ex p33 being Point of (TOP-REAL 2) st
( p1 = p33 & p33 in P & p33 `2 <= 0 ) ;
p1 in P by A3, A11, A13;
then ex p11 being Point of (TOP-REAL 2) st
( p1 = p11 & |.p11.| = 1 ) by A2;
then 1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;
then (- (p1 `2)) ^2 = (p2 `2) ^2 by A15, A17, A16, A18;
then - (p1 `2) = sqrt ((- (p2 `2)) ^2) by A20, SQUARE_1:22;
then - (p1 `2) = - (p2 `2) by A19, SQUARE_1:22;
then p1 = |[(p2 `1),(p2 `2)]| by A15, A17, A16, EUCLID:53
.= p2 by EUCLID:53 ;
hence x = y ; :: thesis: verum

end;

A21: [#] (Closed-Interval-TSpace ((- 1),1)) c= rng g3

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (Closed-Interval-TSpace ((- 1),1)) or x in rng g3 )
assume x in [#] (Closed-Interval-TSpace ((- 1),1)) ; :: thesis: x in rng g3
then A22: x in [.(- 1),1.] by TOPMETR:18;
then reconsider r = x as Real ;
( - 1 <= r & r <= 1 ) by A22, XXREAL_1:1;
then 1 ^2 >= r ^2 by SQUARE_1:49;
then A23: 1 - (r ^2) >= 0 by XREAL_1:48;
set q = |[r,(- (sqrt (1 - (r ^2))))]|;
A24: |[r,(- (sqrt (1 - (r ^2))))]| `2 = - (sqrt (1 - (r ^2))) by EUCLID:52;
|.|[r,(- (sqrt (1 - (r ^2))))]|.| = sqrt (((|[r,(- (sqrt (1 - (r ^2))))]| `1) ^2) + ((|[r,(- (sqrt (1 - (r ^2))))]| `2) ^2)) by JGRAPH_3:1
.= sqrt ((r ^2) + ((|[r,(- (sqrt (1 - (r ^2))))]| `2) ^2)) by EUCLID:52
.= sqrt ((r ^2) + ((- (sqrt (1 - (r ^2)))) ^2)) by EUCLID:52
.= sqrt ((r ^2) + ((sqrt (1 - (r ^2))) ^2)) ;
then |.|[r,(- (sqrt (1 - (r ^2))))]|.| = sqrt ((r ^2) + (1 - (r ^2))) by A23, SQUARE_1:def 2
.= 1 by SQUARE_1:18 ;
then A25: |[r,(- (sqrt (1 - (r ^2))))]| in P by A2;
0 <= sqrt (1 - (r ^2)) by A23, SQUARE_1:def 2;
then |[r,(- (sqrt (1 - (r ^2))))]| in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A25, A24;
then A26: |[r,(- (sqrt (1 - (r ^2))))]| in dom g3 by A2, A11, Th35;
then g3 . |[r,(- (sqrt (1 - (r ^2))))]| = proj1 . |[r,(- (sqrt (1 - (r ^2))))]| by A1
.= |[r,(- (sqrt (1 - (r ^2))))]| `1 by PSCOMP_1:def 5
.= r by EUCLID:52 ;
hence x in rng g3 by A26, FUNCT_1:def 3; :: thesis: verum

end;

A27: Closed-Interval-TSpace ((- 1),1) = R^1 | B by TOPMETR:19;
g2 is continuous by A1, JGRAPH_2:29;
hence ( proj1 | (Lower_Arc P) is continuous Function of ((TOP-REAL 2) | (Lower_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Lower_Arc P) is one-to-one & rng (proj1 | (Lower_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) ) by A21, A27, A12, FUNCT_1:def 4, JGRAPH_1:45, XBOOLE_0:def 10; :: thesis: verum

end;

Lm6: now :: 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 } holds
( proj1 | (Upper_Arc P) is continuous Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Upper_Arc P) is one-to-one & rng (proj1 | (Upper_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) )

reconsider B = [.(- 1),1.] as non empty Subset of R^1 by TOPMETR:17, XXREAL_1:1;
reconsider g = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } implies ( proj1 | (Upper_Arc P) is continuous Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Upper_Arc P) is one-to-one & rng (proj1 | (Upper_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) ) )
set K0 = Upper_Arc P;
reconsider g2 = g | (Upper_Arc P) as Function of ((TOP-REAL 2) | (Upper_Arc P)),R^1 by PRE_TOPC:9;
A1: for p being Point of ((TOP-REAL 2) | (Upper_Arc P)) holds g2 . p = proj1 . p

proof

let p be Point of ((TOP-REAL 2) | (Upper_Arc P)); :: thesis: g2 . p = proj1 . p
p in the carrier of ((TOP-REAL 2) | (Upper_Arc P)) ;
then p in Upper_Arc P by PRE_TOPC:8;
hence g2 . p = proj1 . p by FUNCT_1:49; :: thesis: verum

end;

assume A2: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } ; :: thesis: ( proj1 | (Upper_Arc P) is continuous Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Upper_Arc P) is one-to-one & rng (proj1 | (Upper_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) )
then A3: Upper_Arc P c= P by Th33;
A4: dom g2 = the carrier of ((TOP-REAL 2) | (Upper_Arc P)) by FUNCT_2:def 1;
then A5: dom g2 = Upper_Arc P by PRE_TOPC:8;
rng g2 c= the carrier of (Closed-Interval-TSpace ((- 1),1))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g2 or x in the carrier of (Closed-Interval-TSpace ((- 1),1)) )
assume x in rng g2 ; :: thesis: x in the carrier of (Closed-Interval-TSpace ((- 1),1))
then consider z being object such that
A6: z in dom g2 and
A7: x = g2 . z by FUNCT_1:def 3;
z in P by A5, A3, A6;
then consider p being Point of (TOP-REAL 2) such that
A8: p = z and
A9: |.p.| = 1 by A2;
1 ^2 = ((p `1) ^2) + ((p `2) ^2) by A9, JGRAPH_3:1;
then 1 - ((p `1) ^2) >= 0 by XREAL_1:63;
then - (1 - ((p `1) ^2)) <= 0 ;
then ((p `1) ^2) - 1 <= 0 ;
then A10: ( - 1 <= p `1 & p `1 <= 1 ) by SQUARE_1:43;
x = proj1 . p by A1, A6, A7, A8
.= p `1 by PSCOMP_1:def 5 ;
then x in [.(- 1),1.] by A10, XXREAL_1:1;
hence x in the carrier of (Closed-Interval-TSpace ((- 1),1)) by TOPMETR:18; :: thesis: verum

end;

then reconsider g3 = g2 as Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) by A4, FUNCT_2:2;
dom g3 = [#] ((TOP-REAL 2) | (Upper_Arc P)) by FUNCT_2:def 1;
then A11: dom g3 = Upper_Arc P by PRE_TOPC:def 5;
A12: for x, y being object st x in dom g3 & y in dom g3 & g3 . x = g3 . y holds
x = y

proof

let x, y be object ; :: thesis: ( x in dom g3 & y in dom g3 & g3 . x = g3 . y implies x = y )
assume that
A13: x in dom g3 and
A14: y in dom g3 and
A15: g3 . x = g3 . y ; :: thesis: x = y
reconsider p2 = y as Point of (TOP-REAL 2) by A11, A14;
A16: g3 . y = proj1 . p2 by A1, A14
.= p2 `1 by PSCOMP_1:def 5 ;
reconsider p1 = x as Point of (TOP-REAL 2) by A11, A13;
A17: g3 . x = proj1 . p1 by A1, A13
.= p1 `1 by PSCOMP_1:def 5 ;
p2 in P by A3, A11, A14;
then ex p22 being Point of (TOP-REAL 2) st
( p2 = p22 & |.p22.| = 1 ) by A2;
then A18: 1 ^2 = ((p2 `1) ^2) + ((p2 `2) ^2) by JGRAPH_3:1;
p2 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) } by A2, A11, A14, Th34;
then A19: ex p44 being Point of (TOP-REAL 2) st
( p2 = p44 & p44 in P & p44 `2 >= 0 ) ;
p1 in P by A3, A11, A13;
then ex p11 being Point of (TOP-REAL 2) st
( p1 = p11 & |.p11.| = 1 ) by A2;
then A20: 1 ^2 = ((p1 `1) ^2) + ((p1 `2) ^2) by JGRAPH_3:1;
p1 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) } by A2, A11, A13, Th34;
then ex p33 being Point of (TOP-REAL 2) st
( p1 = p33 & p33 in P & p33 `2 >= 0 ) ;
then p1 `2 = sqrt ((p2 `2) ^2) by A15, A17, A16, A18, A20, SQUARE_1:22;
then p1 `2 = p2 `2 by A19, SQUARE_1:22;
then p1 = |[(p2 `1),(p2 `2)]| by A15, A17, A16, EUCLID:53
.= p2 by EUCLID:53 ;
hence x = y ; :: thesis: verum

end;

A21: [#] (Closed-Interval-TSpace ((- 1),1)) c= rng g3

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] (Closed-Interval-TSpace ((- 1),1)) or x in rng g3 )
assume x in [#] (Closed-Interval-TSpace ((- 1),1)) ; :: thesis: x in rng g3
then A22: x in [.(- 1),1.] by TOPMETR:18;
then reconsider r = x as Real ;
( - 1 <= r & r <= 1 ) by A22, XXREAL_1:1;
then 1 ^2 >= r ^2 by SQUARE_1:49;
then A23: 1 - (r ^2) >= 0 by XREAL_1:48;
set q = |[r,(sqrt (1 - (r ^2)))]|;
A24: |[r,(sqrt (1 - (r ^2)))]| `2 = sqrt (1 - (r ^2)) by EUCLID:52;
|.|[r,(sqrt (1 - (r ^2)))]|.| = sqrt (((|[r,(sqrt (1 - (r ^2)))]| `1) ^2) + ((|[r,(sqrt (1 - (r ^2)))]| `2) ^2)) by JGRAPH_3:1
.= sqrt ((r ^2) + ((|[r,(sqrt (1 - (r ^2)))]| `2) ^2)) by EUCLID:52
.= sqrt ((r ^2) + ((sqrt (1 - (r ^2))) ^2)) by EUCLID:52 ;
then |.|[r,(sqrt (1 - (r ^2)))]|.| = sqrt ((r ^2) + (1 - (r ^2))) by A23, SQUARE_1:def 2
.= 1 by SQUARE_1:18 ;
then A25: |[r,(sqrt (1 - (r ^2)))]| in P by A2;
0 <= sqrt (1 - (r ^2)) by A23, SQUARE_1:def 2;
then |[r,(sqrt (1 - (r ^2)))]| in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A25, A24;
then A26: |[r,(sqrt (1 - (r ^2)))]| in dom g3 by A2, A11, Th34;
then g3 . |[r,(sqrt (1 - (r ^2)))]| = proj1 . |[r,(sqrt (1 - (r ^2)))]| by A1
.= |[r,(sqrt (1 - (r ^2)))]| `1 by PSCOMP_1:def 5
.= r by EUCLID:52 ;
hence x in rng g3 by A26, FUNCT_1:def 3; :: thesis: verum

end;

A27: Closed-Interval-TSpace ((- 1),1) = R^1 | B by TOPMETR:19;
g2 is continuous by A1, JGRAPH_2:29;
hence ( proj1 | (Upper_Arc P) is continuous Function of ((TOP-REAL 2) | (Upper_Arc P)),(Closed-Interval-TSpace ((- 1),1)) & proj1 | (Upper_Arc P) is one-to-one & rng (proj1 | (Upper_Arc P)) = [#] (Closed-Interval-TSpace ((- 1),1)) ) by A21, A27, A12, FUNCT_1:def 4, JGRAPH_1:45, XBOOLE_0:def 10; :: thesis: verum

end;

theorem Th40: :: JGRAPH_5:40

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds
ex f being Function of (Closed-Interval-TSpace ((- 1),1)),((TOP-REAL 2) | (Lower_Arc P)) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
f . (q `1) = q ) & f . (- 1) = W-min P & f . 1 = E-max P )

proof end;

theorem Th41: :: JGRAPH_5:41

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds
ex f being Function of (Closed-Interval-TSpace ((- 1),1)),((TOP-REAL 2) | (Upper_Arc P)) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds
f . (q `1) = q ) & f . (- 1) = W-min P & f . 1 = E-max P )

proof end;

theorem Th42: :: JGRAPH_5:42

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds
ex f being Function of I[01],((TOP-REAL 2) | (Lower_Arc P)) st
( f is being_homeomorphism & ( for q1, q2 being Point of (TOP-REAL 2)
for r1, r2 being Real st f . r1 = q1 & f . r2 = q2 & r1 in [.0,1.] & r2 in [.0,1.] holds
( r1 < r2 iff q1 `1 > q2 `1 ) ) & f . 0 = E-max P & f . 1 = W-min P )

proof end;

theorem Th43: :: JGRAPH_5:43

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds
ex f being Function of I[01],((TOP-REAL 2) | (Upper_Arc P)) st
( f is being_homeomorphism & ( for q1, q2 being Point of (TOP-REAL 2)
for r1, r2 being Real st f . r1 = q1 & f . r2 = q2 & r1 in [.0,1.] & r2 in [.0,1.] holds
( r1 < r2 iff q1 `1 < q2 `1 ) ) & f . 0 = W-min P & f . 1 = E-max P )

proof end;

theorem Th44: :: JGRAPH_5:44

for p1, p2 being 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 } & p2 in Upper_Arc P & LE p1,p2,P holds
p1 in Upper_Arc P

proof end;

theorem Th45: :: JGRAPH_5:45

for p1, p2 being 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 & p1 <> p2 & p1 `1 < 0 & p1 `2 < 0 & p2 `2 < 0 holds
( p1 `1 > p2 `1 & p1 `2 < p2 `2 )

proof end;

theorem Th46: :: JGRAPH_5:46

for p1, p2 being 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 & p1 <> p2 & p2 `1 < 0 & p1 `2 >= 0 & p2 `2 >= 0 holds
( p1 `1 < p2 `1 & p1 `2 < p2 `2 )

proof end;

theorem Th47: :: JGRAPH_5:47

for p1, p2 being 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 & p1 <> p2 & p2 `2 >= 0 holds
p1 `1 < p2 `1

proof end;

theorem Th48: :: JGRAPH_5:48

for p1, p2 being 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 & p1 <> p2 & p1 `2 <= 0 & p1 <> W-min P holds
p1 `1 > p2 `1

proof end;

theorem Th49: :: JGRAPH_5:49

for p1, p2 being 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 } & ( p2 `2 >= 0 or p2 `1 >= 0 ) & LE p1,p2,P & not p1 `2 >= 0 holds
p1 `1 >= 0

proof end;

theorem Th50: :: JGRAPH_5:50

for p1, p2 being 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 & p1 <> p2 & p1 `1 >= 0 & p2 `1 >= 0 holds
p1 `2 > p2 `2

proof end;

theorem Th51: :: JGRAPH_5:51

for p1, p2 being 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 } & p1 in P & p2 in P & p1 `1 < 0 & p2 `1 < 0 & p1 `2 < 0 & p2 `2 < 0 & ( p1 `1 >= p2 `1 or p1 `2 <= p2 `2 ) holds
LE p1,p2,P

proof end;

theorem :: JGRAPH_5:52

for p1, p2 being 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 } & p1 in P & p2 in P & p1 `1 > 0 & p2 `1 > 0 & p1 `2 < 0 & p2 `2 < 0 & ( p1 `1 >= p2 `1 or p1 `2 >= p2 `2 ) holds
LE p1,p2,P

proof end;

theorem Th53: :: JGRAPH_5:53

for p1, p2 being 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 } & p1 in P & p2 in P & p1 `1 < 0 & p2 `1 < 0 & p1 `2 >= 0 & p2 `2 >= 0 & ( p1 `1 <= p2 `1 or p1 `2 <= p2 `2 ) holds
LE p1,p2,P

proof end;

theorem Th54: :: JGRAPH_5:54

for p1, p2 being 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 } & p1 in P & p2 in P & p1 `2 >= 0 & p2 `2 >= 0 & p1 `1 <= p2 `1 holds
LE p1,p2,P

proof end;

theorem Th55: :: JGRAPH_5:55

for p1, p2 being 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 } & p1 in P & p2 in P & p1 `1 >= 0 & p2 `1 >= 0 & p1 `2 >= p2 `2 holds
LE p1,p2,P

proof end;

theorem Th56: :: JGRAPH_5:56

for p1, p2 being 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 } & p1 in P & p2 in P & p1 `2 <= 0 & p2 `2 <= 0 & p2 <> W-min P & p1 `1 >= p2 `1 holds
LE p1,p2,P

proof end;

theorem Th57: :: JGRAPH_5:57

for cn being Real
for q being Point of (TOP-REAL 2) st - 1 < cn & cn < 1 & q `2 <= 0 holds
for p being Point of (TOP-REAL 2) st p = (cn -FanMorphS) . q holds
p `2 <= 0

proof end;

theorem Th58: :: JGRAPH_5:58

for cn being 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

proof end;

theorem Th59: :: JGRAPH_5:59

for p1, p2, p3, p4 being 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 `1 < 0 & p1 `2 >= 0 & p2 `1 < 0 & p2 `2 >= 0 & p3 `1 < 0 & p3 `2 >= 0 & p4 `1 < 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 )

proof end;

theorem Th60: :: JGRAPH_5:60

for p1, p2, p3, p4 being 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 )

proof end;

theorem Th61: :: JGRAPH_5:61

for p1, p2, p3, p4 being 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 )

proof end;

theorem Th62: :: JGRAPH_5:62

for p1, p2, p3, p4 being 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 )

proof end;

theorem Th63: :: JGRAPH_5:63

for p1, p2, p3, p4 being 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 `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 )

proof end;

theorem :: JGRAPH_5:64

for p1, p2, p3, p4 being 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 } & p4 = W-min P & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P 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 )

proof end;

theorem Th65: :: JGRAPH_5:65

for p1, p2, p3, p4 being 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 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 )

proof end;

theorem Th66: :: JGRAPH_5:66

for p1, p2, p3, p4 being 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 <> p2 & p2 <> p3 & p3 <> p4 & p1 `1 < 0 & p2 `1 < 0 & p3 `1 < 0 & p4 `1 < 0 & p1 `2 < 0 & p2 `2 < 0 & p3 `2 < 0 holds
ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & |[(- 1),0]| = f . p1 & |[0,1]| = f . p2 & |[1,0]| = f . p3 & |[0,(- 1)]| = f . p4 )

proof end;

theorem Th67: :: JGRAPH_5:67

for p1, p2, p3, p4 being 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 <> p2 & p2 <> p3 & p3 <> p4 holds
ex f being Function of (TOP-REAL 2),(TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & |[(- 1),0]| = f . p1 & |[0,1]| = f . p2 & |[1,0]| = f . p3 & |[0,(- 1)]| = f . p4 )

proof end;

Lm7: |[(- 1),0]| `1 = - 1
by EUCLID:52;

Lm8: |[(- 1),0]| `2 = 0
by EUCLID:52;

Lm9: ( |[1,0]| `1 = 1 & |[1,0]| `2 = 0 )
by EUCLID:52;

Lm10: |[0,(- 1)]| `1 = 0
by EUCLID:52;

Lm11: |[0,(- 1)]| `2 = - 1
by EUCLID:52;

Lm12: |[0,1]| `1 = 0
by EUCLID:52;

Lm13: |[0,1]| `2 = 1
by EUCLID:52;

Lm14: now :: thesis: ( |.|[(- 1),0]|.| = 1 & |.|[1,0]|.| = 1 & |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )

thus |.|[(- 1),0]|.| = sqrt (((- 1) ^2) + (0 ^2)) by Lm7, Lm8, JGRAPH_3:1
.= 1 by SQUARE_1:18 ; :: thesis: ( |.|[1,0]|.| = 1 & |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )
thus |.|[1,0]|.| = sqrt ((1 ^2) + (0 ^2)) by Lm9, JGRAPH_3:1
.= 1 by SQUARE_1:18 ; :: thesis: ( |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )
thus |.|[0,(- 1)]|.| = sqrt ((0 ^2) + ((- 1) ^2)) by Lm10, Lm11, JGRAPH_3:1
.= 1 by SQUARE_1:18 ; :: thesis: |.|[0,1]|.| = 1
thus |.|[0,1]|.| = sqrt ((0 ^2) + (1 ^2)) by Lm12, Lm13, JGRAPH_3:1
.= 1 by SQUARE_1:18 ; :: thesis: verum

end;

Lm15: 0 in [.0,1.]
by XXREAL_1:1;

Lm16: 1 in [.0,1.]
by XXREAL_1:1;

theorem :: JGRAPH_5:68

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for C0 being 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 holds
for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

proof end;

theorem :: JGRAPH_5:69

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for C0 being 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 holds
for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

proof end;

theorem :: JGRAPH_5:70

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for C0 being 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 holds
for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

proof end;

theorem :: JGRAPH_5:71

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for C0 being 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 holds
for f, g being Function of I[01],(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

proof end;