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

theorem :: JGRAPH_5:1

canceled;

theorem :: JGRAPH_5:2

canceled;

theorem Th3: :: JGRAPH_5:3

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 Th4: :: JGRAPH_5:4

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:5

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 & x in the carrier of PM & x2 in the carrier of PM2 holds
Ball x,r3 c= Ball x2,r3

proof end;

theorem :: JGRAPH_5:6

canceled;

theorem :: JGRAPH_5:7

for a, b being real number
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:27, TOPMETR:30;

theorem Th8: :: JGRAPH_5:8

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 Th9: :: JGRAPH_5:9

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 Th10: :: JGRAPH_5:10

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 Th11: :: JGRAPH_5:11

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 . a = d & h . b = e & d <= e & t1 <= t2 & s1 in [.a,b.] & s2 in [.a,b.] holds
s1 <= s2

proof end;

theorem Th12: :: JGRAPH_5:12

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 . a = e & h . b = d & e >= d & t1 >= t2 & s1 in [.a,b.] & s2 in [.a,b.] holds
s1 <= s2

proof end;

theorem :: JGRAPH_5:13

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

proof end;

theorem Th14: :: JGRAPH_5:14

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.] & 1 in [.0 ,1.] )
by XXREAL_1:1;

theorem Th15: :: JGRAPH_5:15

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 Th16: :: JGRAPH_5:16

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 Th17: :: JGRAPH_5:17

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 Th18: :: JGRAPH_5:18

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 Th19: :: JGRAPH_5:19

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:20

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 Th21: :: JGRAPH_5:21

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:22

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 Th23: :: JGRAPH_5:23

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 Th24: :: JGRAPH_5:24

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 Th25: :: JGRAPH_5:25

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:26

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 Th27: :: JGRAPH_5:27

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 Th28: :: JGRAPH_5:28

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 Th29: :: JGRAPH_5:29

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 Th30: :: JGRAPH_5:30

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;

Lm2: now

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: proj1 .: P c= [.(- 1),1.]

proof

let y be set ; :: 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 set such that
A3: ( x in dom proj1 & x in P & y = proj1 . x ) by FUNCT_1:def 12;
reconsider q = x as Point of (TOP-REAL 2) by A3;
A4: y = q `1 by A3, PSCOMP_1:def 28;
consider q2 being Point of (TOP-REAL 2) such that
A5: ( q2 = x & |.q2.| = 1 ) by A1, A3;
A6: ((q `1 ) ^2 ) + ((q `2 ) ^2 ) = 1 ^2 by A5, JGRAPH_3:10;
0 <= (q `2 ) ^2 by XREAL_1:65;
then (1 - ((q `1 ) ^2 )) + ((q `1 ) ^2 ) >= 0 + ((q `1 ) ^2 ) by A6, XREAL_1:9;
then ( - 1 <= q `1 & q `1 <= 1 ) by SQUARE_1:121;
hence y in [.(- 1),1.] by A4, XXREAL_1:1; :: thesis: verum

end;

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

proof

let y be set ; :: 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
A7: ( y = r & - 1 <= r & r <= 1 ) ;
set q = |[r,(sqrt (1 - (r ^2 )))]|;
A8: dom proj1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A9: ( |[r,(sqrt (1 - (r ^2 )))]| `1 = r & |[r,(sqrt (1 - (r ^2 )))]| `2 = sqrt (1 - (r ^2 )) ) by EUCLID:56;
1 ^2 >= r ^2 by A7, SQUARE_1:119;
then A10: 1 - (r ^2 ) >= 0 by XREAL_1:50;
|.|[r,(sqrt (1 - (r ^2 )))]|.| = sqrt ((r ^2 ) + ((sqrt (1 - (r ^2 ))) ^2 )) by A9, JGRAPH_3:10
.= sqrt ((r ^2 ) + (1 - (r ^2 ))) by A10, SQUARE_1:def 4
.= 1 by SQUARE_1:83 ;
then A11: |[r,(sqrt (1 - (r ^2 )))]| in P by A1;
proj1 . |[r,(sqrt (1 - (r ^2 )))]| = |[r,(sqrt (1 - (r ^2 )))]| `1 by PSCOMP_1:def 28
.= r by EUCLID:56 ;
hence y in proj1 .: P by A7, A8, A11, FUNCT_1:def 12; :: thesis: verum

end;

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

proof

let y be set ; :: 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 set such that
A13: ( x in dom proj2 & x in P & y = proj2 . x ) by FUNCT_1:def 12;
reconsider q = x as Point of (TOP-REAL 2) by A13;
A14: y = q `2 by A13, PSCOMP_1:def 29;
consider q2 being Point of (TOP-REAL 2) such that
A15: ( q2 = x & |.q2.| = 1 ) by A1, A13;
A16: ((q `1 ) ^2 ) + ((q `2 ) ^2 ) = 1 ^2 by A15, JGRAPH_3:10;
0 <= (q `1 ) ^2 by XREAL_1:65;
then (1 - ((q `2 ) ^2 )) + ((q `2 ) ^2 ) >= 0 + ((q `2 ) ^2 ) by A16, XREAL_1:9;
then ( - 1 <= q `2 & q `2 <= 1 ) by SQUARE_1:121;
hence y in [.(- 1),1.] by A14, XXREAL_1:1; :: thesis: verum

end;

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

proof

let y be set ; :: 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
A17: ( y = r & - 1 <= r & r <= 1 ) ;
set q = |[(sqrt (1 - (r ^2 ))),r]|;
A18: dom proj2 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A19: ( |[(sqrt (1 - (r ^2 ))),r]| `2 = r & |[(sqrt (1 - (r ^2 ))),r]| `1 = sqrt (1 - (r ^2 )) ) by EUCLID:56;
1 ^2 >= r ^2 by A17, SQUARE_1:119;
then A20: 1 - (r ^2 ) >= 0 by XREAL_1:50;
|.|[(sqrt (1 - (r ^2 ))),r]|.| = sqrt (((sqrt (1 - (r ^2 ))) ^2 ) + (r ^2 )) by A19, JGRAPH_3:10
.= sqrt ((1 - (r ^2 )) + (r ^2 )) by A20, SQUARE_1:def 4
.= 1 by SQUARE_1:83 ;
then A21: |[(sqrt (1 - (r ^2 ))),r]| in P by A1;
proj2 . |[(sqrt (1 - (r ^2 ))),r]| = |[(sqrt (1 - (r ^2 ))),r]| `2 by PSCOMP_1:def 29
.= r by EUCLID:56 ;
hence y in proj2 .: P by A17, A18, A21, FUNCT_1:def 12; :: thesis: verum

end;

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

end;

Lm3: 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 Th31: :: JGRAPH_5:31

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 Th32: :: JGRAPH_5:32

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 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
E-max P = |[1,0 ]|

proof end;

theorem :: JGRAPH_5:34

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 Th35: :: JGRAPH_5:35

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 Th36: :: JGRAPH_5:36

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 Th37: :: JGRAPH_5:37

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 Th38: :: JGRAPH_5:38

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 Th39: :: JGRAPH_5:39

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 Th40: :: JGRAPH_5:40

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 Th41: :: JGRAPH_5:41

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 Th42: :: JGRAPH_5:42

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;

Lm4: now

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) ) )
assume A1: 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) )
reconsider g = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
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:30;
A2: 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:29;
hence g2 . p = proj1 . p by FUNCT_1:72; :: thesis: verum

end;

then A3: g2 is continuous by JGRAPH_2:39;
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:29;
A6: Lower_Arc P c= P by A1, Th36;
rng g2 c= the carrier of (Closed-Interval-TSpace (- 1),1)

proof

let x be set ; :: 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 set such that
A7: ( z in dom g2 & x = g2 . z ) by FUNCT_1:def 5;
z in P by A5, A6, A7;
then consider p being Point of (TOP-REAL 2) such that
A8: ( p = z & |.p.| = 1 ) by A1;
A9: x = proj1 . p by A2, A7, A8
.= p `1 by PSCOMP_1:def 28 ;
1 ^2 = ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by A8, JGRAPH_3:10;
then 1 - ((p `1 ) ^2 ) >= 0 by XREAL_1:65;
then - (1 - ((p `1 ) ^2 )) <= 0 ;
then ((p `1 ) ^2 ) - 1 <= 0 ;
then ( - 1 <= p `1 & p `1 <= 1 ) by SQUARE_1:112;
then x in [.(- 1),1.] by A9, XXREAL_1:1;
hence x in the carrier of (Closed-Interval-TSpace (- 1),1) by TOPMETR:25; :: 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:4;
dom g3 = [#] ((TOP-REAL 2) | (Lower_Arc P)) by FUNCT_2:def 1;
then A10: dom g3 = Lower_Arc P by PRE_TOPC:def 10;
A11: [#] (Closed-Interval-TSpace (- 1),1) c= rng g3

proof

let x be set ; :: 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 A12: x in [.(- 1),1.] by TOPMETR:25;
then reconsider r = x as Real ;
set q = |[r,(- (sqrt (1 - (r ^2 ))))]|;
A13: |.|[r,(- (sqrt (1 - (r ^2 ))))]|.| = sqrt (((|[r,(- (sqrt (1 - (r ^2 ))))]| `1 ) ^2 ) + ((|[r,(- (sqrt (1 - (r ^2 ))))]| `2 ) ^2 )) by JGRAPH_3:10
.= sqrt ((r ^2 ) + ((|[r,(- (sqrt (1 - (r ^2 ))))]| `2 ) ^2 )) by EUCLID:56
.= sqrt ((r ^2 ) + ((- (sqrt (1 - (r ^2 )))) ^2 )) by EUCLID:56
.= sqrt ((r ^2 ) + ((sqrt (1 - (r ^2 ))) ^2 )) ;
( - 1 <= r & r <= 1 ) by A12, XXREAL_1:1;
then 1 ^2 >= r ^2 by SQUARE_1:119;
then A14: 1 - (r ^2 ) >= 0 by XREAL_1:50;
then 0 <= sqrt (1 - (r ^2 )) by SQUARE_1:def 4;
then A15: - (sqrt (1 - (r ^2 ))) <= 0 ;
|.|[r,(- (sqrt (1 - (r ^2 ))))]|.| = sqrt ((r ^2 ) + (1 - (r ^2 ))) by A13, A14, SQUARE_1:def 4
.= 1 by SQUARE_1:83 ;
then A16: |[r,(- (sqrt (1 - (r ^2 ))))]| in P by A1;
|[r,(- (sqrt (1 - (r ^2 ))))]| `2 = - (sqrt (1 - (r ^2 ))) by EUCLID:56;
then |[r,(- (sqrt (1 - (r ^2 ))))]| in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 <= 0 ) } by A15, A16;
then A17: |[r,(- (sqrt (1 - (r ^2 ))))]| in dom g3 by A1, A10, Th38;
then g3 . |[r,(- (sqrt (1 - (r ^2 ))))]| = proj1 . |[r,(- (sqrt (1 - (r ^2 ))))]| by A2
.= |[r,(- (sqrt (1 - (r ^2 ))))]| `1 by PSCOMP_1:def 28
.= r by EUCLID:56 ;
hence x in rng g3 by A17, FUNCT_1:def 5; :: thesis: verum

end;

reconsider B = [.(- 1),1.] as non empty Subset of R^1 by TOPMETR:24, XXREAL_1:1;
A18: Closed-Interval-TSpace (- 1),1 = R^1 | B by TOPMETR:26;
for x, y being set st x in dom g3 & y in dom g3 & g3 . x = g3 . y holds
x = y

proof

let x, y be set ; :: thesis: ( x in dom g3 & y in dom g3 & g3 . x = g3 . y implies x = y )
assume A19: ( x in dom g3 & y in dom g3 & g3 . x = g3 . y ) ; :: thesis: x = y
then reconsider p1 = x as Point of (TOP-REAL 2) by A10;
reconsider p2 = y as Point of (TOP-REAL 2) by A10, A19;
A20: g3 . x = proj1 . p1 by A2, A19
.= p1 `1 by PSCOMP_1:def 28 ;
A21: g3 . y = proj1 . p2 by A2, A19
.= p2 `1 by PSCOMP_1:def 28 ;
A22: p1 in P by A6, A10, A19;
p2 in P by A6, A10, A19;
then consider p22 being Point of (TOP-REAL 2) such that
A23: ( p2 = p22 & |.p22.| = 1 ) by A1;
A24: 1 ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by A23, JGRAPH_3:10;
consider p11 being Point of (TOP-REAL 2) such that
A25: ( p1 = p11 & |.p11.| = 1 ) by A1, A22;
1 ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by A25, JGRAPH_3:10;
then A26: (- (p1 `2 )) ^2 = (p2 `2 ) ^2 by A19, A20, A21, A24;
p1 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 <= 0 ) } by A1, A10, A19, Th38;
then consider p33 being Point of (TOP-REAL 2) such that
A27: ( p1 = p33 & p33 in P & p33 `2 <= 0 ) ;
- (- (p1 `2 )) <= 0 by A27;
then - (p1 `2 ) >= 0 ;
then A28: - (p1 `2 ) = sqrt ((- (p2 `2 )) ^2 ) by A26, SQUARE_1:89;
p2 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 <= 0 ) } by A1, A10, A19, Th38;
then consider p44 being Point of (TOP-REAL 2) such that
A29: ( p2 = p44 & p44 in P & p44 `2 <= 0 ) ;
- (- (p2 `2 )) <= 0 by A29;
then - (p2 `2 ) >= 0 ;
then - (p1 `2 ) = - (p2 `2 ) by A28, SQUARE_1:89;
then p1 = |[(p2 `1 ),(p2 `2 )]| by A19, A20, A21, EUCLID:57
.= p2 by EUCLID:57 ;
hence x = y ; :: thesis: verum

end;

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 A3, A11, A18, FUNCT_1:def 8, JGRAPH_1:63, XBOOLE_0:def 10; :: thesis: verum

end;

Lm5: now

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) ) )
assume A1: 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) )
reconsider g = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
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:30;
A2: 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:29;
hence g2 . p = proj1 . p by FUNCT_1:72; :: thesis: verum

end;

then A3: g2 is continuous by JGRAPH_2:39;
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:29;
A6: Upper_Arc P c= P by A1, Th36;
rng g2 c= the carrier of (Closed-Interval-TSpace (- 1),1)

proof

let x be set ; :: 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 set such that
A7: ( z in dom g2 & x = g2 . z ) by FUNCT_1:def 5;
z in P by A5, A6, A7;
then consider p being Point of (TOP-REAL 2) such that
A8: ( p = z & |.p.| = 1 ) by A1;
A9: x = proj1 . p by A2, A7, A8
.= p `1 by PSCOMP_1:def 28 ;
1 ^2 = ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by A8, JGRAPH_3:10;
then 1 - ((p `1 ) ^2 ) >= 0 by XREAL_1:65;
then - (1 - ((p `1 ) ^2 )) <= 0 ;
then ((p `1 ) ^2 ) - 1 <= 0 ;
then ( - 1 <= p `1 & p `1 <= 1 ) by SQUARE_1:112;
then x in [.(- 1),1.] by A9, XXREAL_1:1;
hence x in the carrier of (Closed-Interval-TSpace (- 1),1) by TOPMETR:25; :: 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:4;
dom g3 = [#] ((TOP-REAL 2) | (Upper_Arc P)) by FUNCT_2:def 1;
then A10: dom g3 = Upper_Arc P by PRE_TOPC:def 10;
A11: [#] (Closed-Interval-TSpace (- 1),1) c= rng g3

proof

let x be set ; :: 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 A12: x in [.(- 1),1.] by TOPMETR:25;
then reconsider r = x as Real ;
set q = |[r,(sqrt (1 - (r ^2 )))]|;
A13: |.|[r,(sqrt (1 - (r ^2 )))]|.| = sqrt (((|[r,(sqrt (1 - (r ^2 )))]| `1 ) ^2 ) + ((|[r,(sqrt (1 - (r ^2 )))]| `2 ) ^2 )) by JGRAPH_3:10
.= sqrt ((r ^2 ) + ((|[r,(sqrt (1 - (r ^2 )))]| `2 ) ^2 )) by EUCLID:56
.= sqrt ((r ^2 ) + ((sqrt (1 - (r ^2 ))) ^2 )) by EUCLID:56 ;
( - 1 <= r & r <= 1 ) by A12, XXREAL_1:1;
then 1 ^2 >= r ^2 by SQUARE_1:119;
then A14: 1 - (r ^2 ) >= 0 by XREAL_1:50;
then A15: 0 <= sqrt (1 - (r ^2 )) by SQUARE_1:def 4;
|.|[r,(sqrt (1 - (r ^2 )))]|.| = sqrt ((r ^2 ) + (1 - (r ^2 ))) by A13, A14, SQUARE_1:def 4
.= 1 by SQUARE_1:83 ;
then A16: |[r,(sqrt (1 - (r ^2 )))]| in P by A1;
|[r,(sqrt (1 - (r ^2 )))]| `2 = sqrt (1 - (r ^2 )) by EUCLID:56;
then |[r,(sqrt (1 - (r ^2 )))]| in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } by A15, A16;
then A17: |[r,(sqrt (1 - (r ^2 )))]| in dom g3 by A1, A10, Th37;
then g3 . |[r,(sqrt (1 - (r ^2 )))]| = proj1 . |[r,(sqrt (1 - (r ^2 )))]| by A2
.= |[r,(sqrt (1 - (r ^2 )))]| `1 by PSCOMP_1:def 28
.= r by EUCLID:56 ;
hence x in rng g3 by A17, FUNCT_1:def 5; :: thesis: verum

end;

reconsider B = [.(- 1),1.] as non empty Subset of R^1 by TOPMETR:24, XXREAL_1:1;
A18: Closed-Interval-TSpace (- 1),1 = R^1 | B by TOPMETR:26;
for x, y being set st x in dom g3 & y in dom g3 & g3 . x = g3 . y holds
x = y

proof

let x, y be set ; :: thesis: ( x in dom g3 & y in dom g3 & g3 . x = g3 . y implies x = y )
assume A19: ( x in dom g3 & y in dom g3 & g3 . x = g3 . y ) ; :: thesis: x = y
then reconsider p1 = x as Point of (TOP-REAL 2) by A10;
reconsider p2 = y as Point of (TOP-REAL 2) by A10, A19;
A20: g3 . x = proj1 . p1 by A2, A19
.= p1 `1 by PSCOMP_1:def 28 ;
A21: g3 . y = proj1 . p2 by A2, A19
.= p2 `1 by PSCOMP_1:def 28 ;
A22: p1 in P by A6, A10, A19;
p2 in P by A6, A10, A19;
then consider p22 being Point of (TOP-REAL 2) such that
A23: ( p2 = p22 & |.p22.| = 1 ) by A1;
A24: 1 ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by A23, JGRAPH_3:10;
consider p11 being Point of (TOP-REAL 2) such that
A25: ( p1 = p11 & |.p11.| = 1 ) by A1, A22;
A26: 1 ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by A25, JGRAPH_3:10;
p1 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) } by A1, A10, A19, Th37;
then consider p33 being Point of (TOP-REAL 2) such that
A27: ( p1 = p33 & p33 in P & p33 `2 >= 0 ) ;
A28: p1 `2 = sqrt ((p2 `2 ) ^2 ) by A19, A20, A21, A24, A26, A27, SQUARE_1:89;
p2 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 >= 0 ) } by A1, A10, A19, Th37;
then consider p44 being Point of (TOP-REAL 2) such that
A29: ( p2 = p44 & p44 in P & p44 `2 >= 0 ) ;
p1 `2 = p2 `2 by A28, A29, SQUARE_1:89;
then p1 = |[(p2 `1 ),(p2 `2 )]| by A19, A20, A21, EUCLID:57
.= p2 by EUCLID:57 ;
hence x = y ; :: thesis: verum

end;

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 A3, A11, A18, FUNCT_1:def 8, JGRAPH_1:63, XBOOLE_0:def 10; :: thesis: verum

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 (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 Th44: :: JGRAPH_5:44

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 Th45: :: JGRAPH_5:45

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 Th46: :: JGRAPH_5:46

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

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

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

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

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

proof end;

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

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

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 `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: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 < 0 & p2 `2 < 0 & ( p1 `1 >= p2 `1 or 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 `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 Th57: :: JGRAPH_5:57

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 Th58: :: JGRAPH_5:58

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 Th59: :: JGRAPH_5:59

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 Th60: :: JGRAPH_5:60

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 Th61: :: JGRAPH_5:61

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 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 `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 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 & 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 Th64: :: 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 } & 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 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 & ( 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 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 `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: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 } & 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 Th68: :: 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) 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 Th69: :: 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) 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 & p4 `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 Th70: :: 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) 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;

Lm6: ( |[(- 1),0 ]| `1 = - 1 & |[(- 1),0 ]| `2 = 0 & |[1,0 ]| `1 = 1 & |[1,0 ]| `2 = 0 & |[0 ,(- 1)]| `1 = 0 & |[0 ,(- 1)]| `2 = - 1 & |[0 ,1]| `1 = 0 & |[0 ,1]| `2 = 1 )
by EUCLID:56;

Lm7: now

thus |.|[(- 1),0 ]|.| = sqrt (((- 1) ^2 ) + (0 ^2 )) by Lm6, JGRAPH_3:10
.= 1 by SQUARE_1:83 ; :: thesis: ( |.|[1,0 ]|.| = 1 & |.|[0 ,(- 1)]|.| = 1 & |.|[0 ,1]|.| = 1 )
thus |.|[1,0 ]|.| = sqrt ((1 ^2 ) + (0 ^2 )) by Lm6, JGRAPH_3:10
.= 1 by SQUARE_1:83 ; :: thesis: ( |.|[0 ,(- 1)]|.| = 1 & |.|[0 ,1]|.| = 1 )
thus |.|[0 ,(- 1)]|.| = sqrt ((0 ^2 ) + ((- 1) ^2 )) by Lm6, JGRAPH_3:10
.= 1 by SQUARE_1:83 ; :: thesis: |.|[0 ,1]|.| = 1
thus |.|[0 ,1]|.| = sqrt ((0 ^2 ) + (1 ^2 )) by Lm6, JGRAPH_3:10
.= 1 by SQUARE_1:83 ; :: thesis: verum

end;

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

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

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;

theorem :: JGRAPH_5:72

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:73

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:74

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;