:: JGRAPH_5 semantic presentation

Lm1: for a, x being real number st a >= 0 & (x - a) * (x + a) >= 0 & not - a >= x holds
x >= a
by XREAL_1:97;

theorem :: JGRAPH_5:1

canceled;

theorem Th2: :: JGRAPH_5:2

for a, x being real number st a <= 0 & x < a holds
x ^2 > a ^2

proof end;

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 Th6: :: JGRAPH_5:6

for a, b, d, e being real number
for B being Subset of (Closed-Interval-TSpace d,e) st d <= a & a <= b & b <= e & B = [.a,b.] holds
Closed-Interval-TSpace a,b = (Closed-Interval-TSpace d,e) | B

proof end;

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 Th6, TOPMETR:27;

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_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_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_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_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 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;

Lm2: ( 0 in [.0,1.] & 1 in [.0,1.] )
by RCOMP_1:15;

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_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;

Lm3: now

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in proj1 .: P ; :: thesis:
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 by A5, JGRAPH_3:10, SQUARE_1:59;
0 <= (q `2 ) ^2 by SQUARE_1:72;
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 JGRAPH_4:4;
hence y in [.(- 1),1.] by A4, RCOMP_1:48; :: thesis:

end;

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in [.(- 1),1.] ; :: thesis:
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, JGRAPH_2:7;
then A10: 1 - (r ^2 ) >= 0 by XREAL_1:50, SQUARE_1:59;
|.|[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:

end;

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in proj2 .: P ; :: thesis:
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 by A15, JGRAPH_3:10, SQUARE_1:59;
0 <= (q `1 ) ^2 by SQUARE_1:72;
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 JGRAPH_4:4;
hence y in [.(- 1),1.] by A14, RCOMP_1:48; :: thesis:

end;

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in [.(- 1),1.] ; :: thesis:
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, JGRAPH_2:7;
then A20: 1 - (r ^2 ) >= 0 by XREAL_1:50, SQUARE_1:59;
|.|[(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:

end;

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

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 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_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_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_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_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

let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
assume A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } ; :: thesis:
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 JGRAPH_3:12;
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:
p in the carrier of ((TOP-REAL 2) | (Lower_Arc P)) ;
then p in Lower_Arc P by JORDAN1:1;
hence g2 . p = proj1 . p by FUNCT_1:72; :: thesis:

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 JORDAN1:1;
A6: Lower_Arc P c= P by A1, Th36;
A7: rng g2 c= the carrier of (Closed-Interval-TSpace (- 1),1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng g2 ; :: thesis:
then consider z being set such that
A8: ( z in dom g2 & x = g2 . z ) by FUNCT_1:def 5;
z in P by A5, A6, A8;
then consider p being Point of (TOP-REAL 2) such that
A9: ( p = z & |.p.| = 1 ) by A1;
A10: x = proj1 . p by A2, A4, A8, A9
.= p `1 by PSCOMP_1:def 28 ;
1 = ((p `1 ) ^2 ) + ((p `2 ) ^2 ) by A9, JGRAPH_3:10, SQUARE_1:59;
then 1 - ((p `1 ) ^2 ) >= 0 by SQUARE_1:72;
then - (1 - ((p `1 ) ^2 )) <= 0 by XREAL_1:60;
then ((p `1 ) ^2 ) - 1 <= 0 ;
then ( - 1 <= p `1 & p `1 <= 1 ) by JGRAPH_3:5;
then x in [.(- 1),1.] by A10, RCOMP_1:48;
hence x in the carrier of (Closed-Interval-TSpace (- 1),1) by TOPMETR:25; :: thesis:

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 = the carrier of ((TOP-REAL 2) | (Lower_Arc P)) by FUNCT_2:def 1;
then dom g3 = [#] ((TOP-REAL 2) | (Lower_Arc P)) by PRE_TOPC:12;
then A11: dom g3 = Lower_Arc P by PRE_TOPC:def 10;
A12: rng g2 c= [#] (Closed-Interval-TSpace (- 1),1) by A7, PRE_TOPC:12;
A13: [#] (Closed-Interval-TSpace (- 1),1) c= rng g3

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in [#] (Closed-Interval-TSpace (- 1),1) ; :: thesis:
then x in the carrier of (Closed-Interval-TSpace (- 1),1) ;
then A14: x in [.(- 1),1.] by TOPMETR:25;
then reconsider r = x as Real ;
set q = |[r,(- (sqrt (1 - (r ^2 ))))]|;
A15: |.|[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 )) by SQUARE_1:61 ;
( - 1 <= r & r <= 1 ) by A14, RCOMP_1:48;
then 1 ^2 >= r ^2 by JGRAPH_2:7;
then A16: 1 - (r ^2 ) >= 0 by XREAL_1:50, SQUARE_1:59;
then 0 <= sqrt (1 - (r ^2 )) by SQUARE_1:def 4;
then A17: - (sqrt (1 - (r ^2 ))) <= 0 by XREAL_1:60;
|.|[r,(- (sqrt (1 - (r ^2 ))))]|.| = sqrt ((r ^2 ) + (1 - (r ^2 ))) by A15, A16, SQUARE_1:def 4
.= 1 by SQUARE_1:83 ;
then A18: |[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 A17, A18;
then A19: |[r,(- (sqrt (1 - (r ^2 ))))]| in dom g3 by A1, A11, Th38;
then g3 . |[r,(- (sqrt (1 - (r ^2 ))))]| = proj1 . |[r,(- (sqrt (1 - (r ^2 ))))]| by A2, A4
.= |[r,(- (sqrt (1 - (r ^2 ))))]| `1 by PSCOMP_1:def 28
.= r by EUCLID:56 ;
hence x in rng g3 by A19, FUNCT_1:def 5; :: thesis:

end;

reconsider B = [.(- 1),1.] as non empty Subset of R^1 by TOPMETR:24, RCOMP_1:48;
A20: 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:
assume A21: ( x in dom g3 & y in dom g3 & g3 . x = g3 . y ) ; :: thesis:
then reconsider p1 = x as Point of (TOP-REAL 2) by A11;
reconsider p2 = y as Point of (TOP-REAL 2) by A11, A21;
A22: g3 . x = proj1 . p1 by A2, A4, A21
.= p1 `1 by PSCOMP_1:def 28 ;
A23: g3 . y = proj1 . p2 by A2, A4, A21
.= p2 `1 by PSCOMP_1:def 28 ;
A24: p1 in P by A6, A11, A21;
p2 in P by A6, A11, A21;
then consider p22 being Point of (TOP-REAL 2) such that
A25: ( p2 = p22 & |.p22.| = 1 ) by A1;
1 ^2 = ((p2 `1 ) ^2 ) + ((p2 `2 ) ^2 ) by A25, JGRAPH_3:10;
then A26: (1 ^2 ) - ((p2 `1 ) ^2 ) = (p2 `2 ) ^2 ;
consider p11 being Point of (TOP-REAL 2) such that
A27: ( p1 = p11 & |.p11.| = 1 ) by A1, A24;
1 ^2 = ((p1 `1 ) ^2 ) + ((p1 `2 ) ^2 ) by A27, JGRAPH_3:10;
then (1 ^2 ) - ((p1 `1 ) ^2 ) = (p1 `2 ) ^2 ;
then (- (p1 `2 )) ^2 = (p2 `2 ) ^2 by A21, A22, A23, A26, SQUARE_1:61;
then A28: (- (p1 `2 )) ^2 = (- (p2 `2 )) ^2 by SQUARE_1:61;
p1 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 <= 0 ) } by A1, A11, A21, Th38;
then consider p33 being Point of (TOP-REAL 2) such that
A29: ( p1 = p33 & p33 in P & p33 `2 <= 0 ) ;
- (- (p1 `2 )) <= 0 by A29;
then - (p1 `2 ) >= 0 by XREAL_1:60;
then A30: - (p1 `2 ) = sqrt ((- (p2 `2 )) ^2 ) by A28, SQUARE_1:89;
p2 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 in P & p3 `2 <= 0 ) } by A1, A11, A21, Th38;
then consider p44 being Point of (TOP-REAL 2) such that
A31: ( p2 = p44 & p44 in P & p44 `2 <= 0 ) ;
- (- (p2 `2 )) <= 0 by A31;
then - (p2 `2 ) >= 0 by XREAL_1:60;
then - (p1 `2 ) = - (p2 `2 ) by A30, SQUARE_1:89;
then - (- (p1 `2 )) = p2 `2 ;
then p1 = |[(p2 `1 ),(p2 `2 )]| by A21, A22, A23, EUCLID:57
.= p2 by EUCLID:57 ;
hence x = y ; :: thesis:

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, A12, A13, A20, FUNCT_1:def 8, JGRAPH_1:63, XBOOLE_0:def 10; :: thesis:

end;

Lm6: now

let P be non empty compact Subset of (TOP-REAL 2); :: thesis:
assume A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } ; :: thesis:
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 JGRAPH_3:12;
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:
p in the carrier of ((TOP-REAL 2) | (Upper_Arc P)) ;
then p in Upper_Arc P by JORDAN1:1;
hence g2 . p = proj1 . p by FUNCT_1:72; :: thesis:

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 JORDAN1:1;
A6: Upper_Arc P c= P by A1, Th36;
A7: rng g2 c= the carrier of (Closed-Interval-TSpace (- 1),1)

proof

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 = the carrier of ((TOP-REAL 2) | (Upper_Arc P)) by FUNCT_2:def 1;
then dom g3 = [#] ((TOP-REAL 2) | (Upper_Arc P)) by PRE_TOPC:12;
then A11: dom g3 = Upper_Arc P by PRE_TOPC:def 10;
A12: rng g2 c= [#] (Closed-Interval-TSpace (- 1),1) by A7, PRE_TOPC:12;
A13: [#] (Closed-Interval-TSpace (- 1),1) c= rng g3

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in [#] (Closed-Interval-TSpace (- 1),1) ; :: thesis:
then x in the carrier of (Closed-Interval-TSpace (- 1),1) ;
then A14: x in [.(- 1),1.] by TOPMETR:25;
then reconsider r = x as Real ;
set q = |[r,(sqrt (1 - (r ^2 )))]|;
A15: |.|[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 A14, RCOMP_1:48;
then 1 ^2 >= r ^2 by JGRAPH_2:7;
then A16: 1 - (r ^2 ) >= 0 by XREAL_1:50, SQUARE_1:59;
then A17: 0 <= sqrt (1 - (r ^2 )) by SQUARE_1:def 4;
|.|[r,(sqrt (1 - (r ^2 )))]|.| = sqrt ((r ^2 ) + (1 - (r ^2 ))) by A15, A16, SQUARE_1:def 4
.= 1 by SQUARE_1:83 ;
then A18: |[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 A17, A18;
then A19: |[r,(sqrt (1 - (r ^2 )))]| in dom g3 by A1, A11, Th37;
then g3 . |[r,(sqrt (1 - (r ^2 )))]| = proj1 . |[r,(sqrt (1 - (r ^2 )))]| by A2, A4
.= |[r,(sqrt (1 - (r ^2 )))]| `1 by PSCOMP_1:def 28
.= r by EUCLID:56 ;
hence x in rng g3 by A19, FUNCT_1:def 5; :: thesis:

end;

proof

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

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, A12, A13, A20, FUNCT_1:def 8, JGRAPH_1:63, XBOOLE_0:def 10; :: thesis:

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_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_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_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_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_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_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_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_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_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_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_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_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_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 & |[(- 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;

Lm8: now

thus |.|[(- 1),0]|.| = sqrt (((- 1) ^2 ) + (0 ^2 )) by Lm7, JGRAPH_3:10
.= 1 by SQUARE_1:59, SQUARE_1:60, SQUARE_1:61, SQUARE_1:83 ; :: thesis:
thus |.|[1,0]|.| = sqrt (1 + 0) by Lm7, JGRAPH_3:10, SQUARE_1:59, SQUARE_1:60
.= 1 by SQUARE_1:83 ; :: thesis:
thus |.|[0,(- 1)]|.| = sqrt ((0 ^2 ) + ((- 1) ^2 )) by Lm7, JGRAPH_3:10
.= 1 by SQUARE_1:59, SQUARE_1:60, SQUARE_1:61, SQUARE_1:83 ; :: thesis:
thus |.|[0,1]|.| = sqrt ((0 ^2 ) + (1 ^2 )) by Lm7, JGRAPH_3:10
.= 1 by SQUARE_1:59, SQUARE_1:60, SQUARE_1:83 ; :: thesis:

end;

Lm9: 0 in [.0,1.]
by RCOMP_1:48;

Lm10: 1 in [.0,1.]
by RCOMP_1:48;

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;