:: 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 () 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 () 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 ;

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 (),() 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 (),() 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. ()) = 0. ()
proof end;

theorem Th11: :: JGRAPH_5:11
for f, g being Function of I[01],()
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],() st f is continuous & f is one-to-one holds
ex f2 being Function of I[01],() 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],()
for C0, KXP, KXN, KYP, KYN being Subset of ()
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 () : |.p.| <= 1 } & KXP = { q1 where q1 is Point of () : ( |.q1.| = 1 & q1 2 <= q1 1 & q1 2 >= - (q1 1) ) } & KXN = { q2 where q2 is Point of () : ( |.q2.| = 1 & q2 2 >= q2 1 & q2 2 <= - (q2 1) ) } & KYP = { q3 where q3 is Point of () : ( |.q3.| = 1 & q3 2 >= q3 1 & q3 2 >= - (q3 1) ) } & KYN = { q4 where q4 is Point of () : ( |.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],()
for C0, KXP, KXN, KYP, KYN being Subset of ()
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 () : |.p.| >= 1 } & KXP = { q1 where q1 is Point of () : ( |.q1.| = 1 & q1 2 <= q1 1 & q1 2 >= - (q1 1) ) } & KXN = { q2 where q2 is Point of () : ( |.q2.| = 1 & q2 2 >= q2 1 & q2 2 <= - (q2 1) ) } & KYP = { q3 where q3 is Point of () : ( |.q3.| = 1 & q3 2 >= q3 1 & q3 2 >= - (q3 1) ) } & KYN = { q4 where q4 is Point of () : ( |.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],()
for C0, KXP, KXN, KYP, KYN being Subset of ()
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 () : |.p.| >= 1 } & KXP = { q1 where q1 is Point of () : ( |.q1.| = 1 & q1 2 <= q1 1 & q1 2 >= - (q1 1) ) } & KXN = { q2 where q2 is Point of () : ( |.q2.| = 1 & q2 2 >= q2 1 & q2 2 <= - (q2 1) ) } & KYP = { q3 where q3 is Point of () : ( |.q3.| = 1 & q3 2 >= q3 1 & q3 2 >= - (q3 1) ) } & KYN = { q4 where q4 is Point of () : ( |.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],()
for C0 being Subset of () st C0 = { q where q is Point of () : |.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 ()
for C0 being Subset of () st C0 = { p where p is Point of () : |.p.| >= 1 } & |.p1.| = 1 & |.p2.| = 1 & |.p3.| = 1 & |.p4.| = 1 & ex h being Function of (),() 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],() 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 () st - 1 < cn & cn < 1 & q 2 > 0 holds
for p being Point of () st p = () . q holds
p 2 > 0
proof end;

theorem :: JGRAPH_5:19
for cn being Real
for q being Point of () st - 1 < cn & cn < 1 & q 2 >= 0 holds
for p being Point of () st p = () . q holds
p 2 >= 0
proof end;

theorem Th20: :: JGRAPH_5:20
for cn being Real
for q being Point of () st - 1 < cn & cn < 1 & q 2 >= 0 & (q 1) / |.q.| < cn & |.q.| <> 0 holds
for p being Point of () st p = () . 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 () 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 () st p1 = () . q1 & p2 = () . q2 holds
(p1 1) / |.p1.| < (p2 1) / |.p2.|
proof end;

theorem Th22: :: JGRAPH_5:22
for sn being Real
for q being Point of () st - 1 < sn & sn < 1 & q 1 > 0 holds
for p being Point of () st p = () . q holds
p 1 > 0
proof end;

theorem :: JGRAPH_5:23
for sn being Real
for q being Point of () st - 1 < sn & sn < 1 & q 1 >= 0 & (q 2) / |.q.| < sn & |.q.| <> 0 holds
for p being Point of () st p = () . 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 () 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 () st p1 = () . q1 & p2 = () . q2 holds
(p1 2) / |.p1.| < (p2 2) / |.p2.|
proof end;

theorem Th25: :: JGRAPH_5:25
for cn being Real
for q being Point of () st - 1 < cn & cn < 1 & q 2 < 0 holds
for p being Point of () st p = () . q holds
p 2 < 0
proof end;

theorem Th26: :: JGRAPH_5:26
for cn being Real
for q being Point of () st - 1 < cn & cn < 1 & q 2 < 0 & (q 1) / |.q.| > cn holds
for p being Point of () st p = () . 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 () 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 () st p1 = () . q1 & p2 = () . q2 holds
(p1 1) / |.p1.| < (p2 1) / |.p2.|
proof end;

Lm3: now :: thesis: for P being non empty compact Subset of () st P = { q where q is Point of () : |.q.| = 1 } holds
( proj1 .: P = [.(- 1),1.] & proj2 .: P = [.(- 1),1.] )
let P be non empty compact Subset of (); :: thesis: ( P = { q where q is Point of () : |.q.| = 1 } implies ( proj1 .: P = [.(- 1),1.] & proj2 .: P = [.(- 1),1.] ) )
assume A1: P = { q where q is Point of () : |.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:
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 ;
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
.= 1 by SQUARE_1:18 ;
then A6: ( dom proj1 = the carrier of () & |[r,(sqrt (1 - (r ^2)))]| in P ) by ;
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 ; :: 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 () by A7;
ex q2 being Point of () 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 ;
then A11: ( - 1 <= q 1 & q 1 <= 1 ) by SQUARE_1:51;
y = q 1 by ;
hence y in [.(- 1),1.] by ; :: thesis: verum
end;
hence proj1 .: P = [.(- 1),1.] by ; :: 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:
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 ;
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
.= 1 by SQUARE_1:18 ;
then A16: ( dom proj2 = the carrier of () & |[(sqrt (1 - (r ^2))),r]| in P ) by ;
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 ; :: 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 () by A17;
ex q2 being Point of () st
( q2 = x & |.q2.| = 1 ) by ;
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 ;
then A21: ( - 1 <= q 2 & q 2 <= 1 ) by SQUARE_1:51;
y = q 2 by ;
hence y in [.(- 1),1.] by ; :: thesis: verum
end;
hence proj2 .: P = [.(- 1),1.] by ; :: thesis: verum
end;

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

proof end;

theorem Th28: :: JGRAPH_5:28
for P being non empty compact Subset of () st P = { q where q is Point of () : |.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 () st P = { q where q is Point of () : |.q.| = 1 } holds
W-min P = |[(- 1),0]|
proof end;

theorem Th30: :: JGRAPH_5:30
for P being non empty compact Subset of () st P = { q where q is Point of () : |.q.| = 1 } holds
E-max P = |[1,0]|
proof end;

theorem :: JGRAPH_5:31
for f being Function of (),R^1 st ( for p being Point of () holds f . p = proj1 . p ) holds
f is continuous
proof end;

theorem Th32: :: JGRAPH_5:32
for f being Function of (),R^1 st ( for p being Point of () holds f . p = proj2 . p ) holds
f is continuous
proof end;

theorem Th33: :: JGRAPH_5:33
for P being non empty compact Subset of () st P = { q where q is Point of () : |.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 () st P = { q where q is Point of () : |.q.| = 1 } holds
Upper_Arc P = { p where p is Point of () : ( p in P & p 2 >= 0 ) }
proof end;

theorem Th35: :: JGRAPH_5:35
for P being non empty compact Subset of () st P = { q where q is Point of () : |.q.| = 1 } holds
Lower_Arc P = { p where p is Point of () : ( 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 (((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 (((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 () st P = { p where p is Point of () : |.p.| = 1 } holds
( proj1 | () is continuous Function of (() | ()),(Closed-Interval-TSpace ((- 1),1)) & proj1 | () is one-to-one & rng (proj1 | ()) = [#] (Closed-Interval-TSpace ((- 1),1)) )
reconsider B = [.(- 1),1.] as non empty Subset of R^1 by ;
reconsider g = proj1 as Function of (),R^1 by TOPMETR:17;
let P be non empty compact Subset of (); :: thesis: ( P = { p where p is Point of () : |.p.| = 1 } implies ( proj1 | () is continuous Function of (() | ()),(Closed-Interval-TSpace ((- 1),1)) & proj1 | () is one-to-one & rng (proj1 | ()) = [#] (Closed-Interval-TSpace ((- 1),1)) ) )
set K0 = Lower_Arc P;
reconsider g2 = g | () as Function of (() | ()),R^1 by PRE_TOPC:9;
A1: for p being Point of (() | ()) holds g2 . p = proj1 . p
proof
let p be Point of (() | ()); :: thesis: g2 . p = proj1 . p
p in the carrier of (() | ()) ;
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 () : |.p.| = 1 } ; :: thesis: ( proj1 | () is continuous Function of (() | ()),(Closed-Interval-TSpace ((- 1),1)) & proj1 | () is one-to-one & rng (proj1 | ()) = [#] (Closed-Interval-TSpace ((- 1),1)) )
then A3: Lower_Arc P c= P by Th33;
A4: dom g2 = the carrier of (() | ()) 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 () such that
A8: p = z and
A9: |.p.| = 1 by A2;
1 ^2 = ((p 1) ^2) + ((p 2) ^2) by ;
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 ;
hence x in the carrier of (Closed-Interval-TSpace ((- 1),1)) by TOPMETR:18; :: thesis: verum
end;
then reconsider g3 = g2 as Function of (() | ()),(Closed-Interval-TSpace ((- 1),1)) by ;
dom g3 = [#] (() | ()) 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 () by ;
A16: g3 . y = proj1 . p2 by
.= p2 1 by PSCOMP_1:def 5 ;
reconsider p1 = x as Point of () by ;
A17: g3 . x = proj1 . p1 by
.= p1 1 by PSCOMP_1:def 5 ;
p2 in P by A3, A11, A14;
then ex p22 being Point of () 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 () : ( p3 in P & p3 2 <= 0 ) } by A2, A11, A14, Th35;
then A19: ex p44 being Point of () st
( p2 = p44 & p44 in P & p44 2 <= 0 ) ;
p1 in { p3 where p3 is Point of () : ( p3 in P & p3 2 <= 0 ) } by A2, A11, A13, Th35;
then A20: ex p33 being Point of () st
( p1 = p33 & p33 in P & p33 2 <= 0 ) ;
p1 in P by A3, A11, A13;
then ex p11 being Point of () 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 ;
then - (p1 2) = - (p2 2) by ;
then p1 = |[(p2 1),(p2 2)]| by
.= 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 ;
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
.= 1 by SQUARE_1:18 ;
then A25: |[r,(- (sqrt (1 - (r ^2))))]| in P by A2;
0 <= sqrt (1 - (r ^2)) by ;
then |[r,(- (sqrt (1 - (r ^2))))]| in { p where p is Point of () : ( p in P & p 2 <= 0 ) } by ;
then A26: |[r,(- (sqrt (1 - (r ^2))))]| in dom g3 by ;
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 ; :: thesis: verum
end;
A27: Closed-Interval-TSpace ((- 1),1) = R^1 | B by TOPMETR:19;
g2 is continuous by ;
hence ( proj1 | () is continuous Function of (() | ()),(Closed-Interval-TSpace ((- 1),1)) & proj1 | () is one-to-one & rng (proj1 | ()) = [#] (Closed-Interval-TSpace ((- 1),1)) ) by ; :: thesis: verum
end;

Lm6: now :: thesis: for P being non empty compact Subset of () st P = { p where p is Point of () : |.p.| = 1 } holds
( proj1 | () is continuous Function of (() | ()),(Closed-Interval-TSpace ((- 1),1)) & proj1 | () is one-to-one & rng (proj1 | ()) = [#] (Closed-Interval-TSpace ((- 1),1)) )
reconsider B = [.(- 1),1.] as non empty Subset of R^1 by ;
reconsider g = proj1 as Function of (),R^1 by TOPMETR:17;
let P be non empty compact Subset of (); :: thesis: ( P = { p where p is Point of () : |.p.| = 1 } implies ( proj1 | () is continuous Function of (() | ()),(Closed-Interval-TSpace ((- 1),1)) & proj1 | () is one-to-one & rng (proj1 | ()) = [#] (Closed-Interval-TSpace ((- 1),1)) ) )
set K0 = Upper_Arc P;
reconsider g2 = g | () as Function of (() | ()),R^1 by PRE_TOPC:9;
A1: for p being Point of (() | ()) holds g2 . p = proj1 . p
proof
let p be Point of (() | ()); :: thesis: g2 . p = proj1 . p
p in the carrier of (() | ()) ;
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 () : |.p.| = 1 } ; :: thesis: ( proj1 | () is continuous Function of (() | ()),(Closed-Interval-TSpace ((- 1),1)) & proj1 | () is one-to-one & rng (proj1 | ()) = [#] (Closed-Interval-TSpace ((- 1),1)) )
then A3: Upper_Arc P c= P by Th33;
A4: dom g2 = the carrier of (() | ()) 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 () such that
A8: p = z and
A9: |.p.| = 1 by A2;
1 ^2 = ((p 1) ^2) + ((p 2) ^2) by ;
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 ;
hence x in the carrier of (Closed-Interval-TSpace ((- 1),1)) by TOPMETR:18; :: thesis: verum
end;
then reconsider g3 = g2 as Function of (() | ()),(Closed-Interval-TSpace ((- 1),1)) by ;
dom g3 = [#] (() | ()) 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 () by ;
A16: g3 . y = proj1 . p2 by
.= p2 1 by PSCOMP_1:def 5 ;
reconsider p1 = x as Point of () by ;
A17: g3 . x = proj1 . p1 by
.= p1 1 by PSCOMP_1:def 5 ;
p2 in P by A3, A11, A14;
then ex p22 being Point of () 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 () : ( p3 in P & p3 2 >= 0 ) } by A2, A11, A14, Th34;
then A19: ex p44 being Point of () st
( p2 = p44 & p44 in P & p44 2 >= 0 ) ;
p1 in P by A3, A11, A13;
then ex p11 being Point of () 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 () : ( p3 in P & p3 2 >= 0 ) } by A2, A11, A13, Th34;
then ex p33 being Point of () st
( p1 = p33 & p33 in P & p33 2 >= 0 ) ;
then p1 2 = sqrt ((p2 2) ^2) by ;
then p1 2 = p2 2 by ;
then p1 = |[(p2 1),(p2 2)]| by
.= 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 ;
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
.= 1 by SQUARE_1:18 ;
then A25: |[r,(sqrt (1 - (r ^2)))]| in P by A2;
0 <= sqrt (1 - (r ^2)) by ;
then |[r,(sqrt (1 - (r ^2)))]| in { p where p is Point of () : ( p in P & p 2 >= 0 ) } by ;
then A26: |[r,(sqrt (1 - (r ^2)))]| in dom g3 by ;
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 ; :: thesis: verum
end;
A27: Closed-Interval-TSpace ((- 1),1) = R^1 | B by TOPMETR:19;
g2 is continuous by ;
hence ( proj1 | () is continuous Function of (() | ()),(Closed-Interval-TSpace ((- 1),1)) & proj1 | () is one-to-one & rng (proj1 | ()) = [#] (Closed-Interval-TSpace ((- 1),1)) ) by ; :: thesis: verum
end;

theorem Th40: :: JGRAPH_5:40
for P being non empty compact Subset of () st P = { p where p is Point of () : |.p.| = 1 } holds
ex f being Function of (Closed-Interval-TSpace ((- 1),1)),(() | ()) st
( f is being_homeomorphism & ( for q being Point of () 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 () st P = { p where p is Point of () : |.p.| = 1 } holds
ex f being Function of (Closed-Interval-TSpace ((- 1),1)),(() | ()) st
( f is being_homeomorphism & ( for q being Point of () 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 () st P = { p where p is Point of () : |.p.| = 1 } holds
ex f being Function of I[01],(() | ()) st
( f is being_homeomorphism & ( for q1, q2 being Point of ()
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 () st P = { p where p is Point of () : |.p.| = 1 } holds
ex f being Function of I[01],(() | ()) st
( f is being_homeomorphism & ( for q1, q2 being Point of ()
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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 () st - 1 < cn & cn < 1 & q 2 <= 0 holds
for p being Point of () st p = () . q holds
p 2 <= 0
proof end;

theorem Th58: :: JGRAPH_5:58
for cn being Real
for p1, p2, q1, q2 being Point of ()
for P being non empty compact Subset of () st - 1 < cn & cn < 1 & P = { p where p is Point of () : |.p.| = 1 } & LE p1,p2,P & q1 = () . p1 & q2 = () . p2 holds
LE q1,q2,P
proof end;

theorem Th59: :: JGRAPH_5:59
for p1, p2, p3, p4 being Point of ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 (),() ex q1, q2, q3, q4 being Point of () st
( f is being_homeomorphism & ( for q being Point of () 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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 (),() ex q1, q2, q3, q4 being Point of () st
( f is being_homeomorphism & ( for q being Point of () 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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 (),() ex q1, q2, q3, q4 being Point of () st
( f is being_homeomorphism & ( for q being Point of () 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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 (),() ex q1, q2, q3, q4 being Point of () st
( f is being_homeomorphism & ( for q being Point of () 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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 (),() ex q1, q2, q3, q4 being Point of () st
( f is being_homeomorphism & ( for q being Point of () 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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.p.| = 1 } & p4 = W-min P & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
ex f being Function of (),() ex q1, q2, q3, q4 being Point of () st
( f is being_homeomorphism & ( for q being Point of () 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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
ex f being Function of (),() ex q1, q2, q3, q4 being Point of () st
( f is being_homeomorphism & ( for q being Point of () 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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 (),() st
( f is being_homeomorphism & ( for q being Point of () 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 ()
for P being non empty compact Subset of () st P = { p where p is Point of () : |.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 (),() st
( f is being_homeomorphism & ( for q being Point of () 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:
by EUCLID:52;

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

Lm14: now :: thesis: ( |.|[(- 1),0]|.| = 1 & = 1 & |.|[0,(- 1)]|.| = 1 & = 1 )
thus |.|[(- 1),0]|.| = sqrt (((- 1) ^2) + ()) by
.= 1 by SQUARE_1:18 ; :: thesis: ( = 1 & |.|[0,(- 1)]|.| = 1 & = 1 )
thus = sqrt ((1 ^2) + ()) by
.= 1 by SQUARE_1:18 ; :: thesis: ( |.|[0,(- 1)]|.| = 1 & = 1 )
thus |.|[0,(- 1)]|.| = sqrt (() + ((- 1) ^2)) by
.= 1 by SQUARE_1:18 ; :: thesis: = 1
thus = sqrt (() + (1 ^2)) by
.= 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 ()
for P being non empty compact Subset of ()
for C0 being Subset of () st P = { p where p is Point of () : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of ()
for C0 being Subset of () st P = { p where p is Point of () : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of ()
for C0 being Subset of () st P = { p where p is Point of () : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of () : |.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 ()
for P being non empty compact Subset of ()
for C0 being Subset of () st P = { p where p is Point of () : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
for f, g being Function of I[01],() st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of () : |.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;