:: JGRAPH_5 semantic presentation

Lemma1: for b₁, b₂ being real number st b₁ >= 0 & (b₂ - b₁) * (b₂ + b₁) >= 0 & not - b₁ >= b₂ holds
b₂ >= b₁
by XREAL_1:97;

theorem Th1: :: JGRAPH_5:1

canceled;

theorem Th2: :: JGRAPH_5:2

for b₁, b₂ being real number st b₁ <= 0 & b₂ < b₁ holds
b₂ ^2 > b₁ ^2

proof end;

theorem Th3: :: JGRAPH_5:3

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

proof end;

theorem Th4: :: JGRAPH_5:4

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

proof end;

theorem Th5: :: JGRAPH_5:5

for b₁, b₂, b₃, b₄, b₅ being Real
for b₆, b₇ being non empty MetrStruct
for b₈ being Element of b₆
for b₉ being Element of b₇ st b₃ <= b₁ & b₁ <= b₂ & b₂ <= b₄ & b₆ = Closed-Interval-MSpace b₁,b₂ & b₇ = Closed-Interval-MSpace b₃,b₄ & b₈ = b₉ & b₈ in the carrier of b₆ & b₉ in the carrier of b₇ holds
Ball b₈,b₅ c= Ball b₉,b₅

proof end;

theorem Th6: :: JGRAPH_5:6

for b₁, b₂, b₃, b₄ being real number
for b₅ being Subset of (Closed-Interval-TSpace b₃,b₄) st b₃ <= b₁ & b₁ <= b₂ & b₂ <= b₄ & b₅ = [.b₁,b₂.] holds
Closed-Interval-TSpace b₁,b₂ = (Closed-Interval-TSpace b₃,b₄) | b₅

proof end;

theorem Th7: :: JGRAPH_5:7

for b₁, b₂ being real number
for b₃ being Subset of I[01] st 0 <= b₁ & b₁ <= b₂ & b₂ <= 1 & b₃ = [.b₁,b₂.] holds
Closed-Interval-TSpace b₁,b₂ = I[01] | b₃ by Th6, TOPMETR:27;

theorem Th8: :: JGRAPH_5:8

for b₁ being TopStruct
for b₂, b₃ being non empty TopStruct
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₅ is_homeomorphism & b₄ is continuous holds
b₅ * b₄ is continuous

proof end;

theorem Th9: :: JGRAPH_5:9

for b₁, b₂, b₃ being TopStruct
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₅ is_homeomorphism & b₄ is one-to-one holds
b₅ * b₄ is one-to-one

proof end;

theorem Th10: :: JGRAPH_5:10

for b₁ being TopStruct
for b₂, b₃ being non empty TopStruct
for b₄ being non empty Subset of b₂
for b₅ being Function of b₁,(b₂ | b₄)
for b₆ being Function of b₂,b₃
for b₇ being Function of b₁,b₃ st b₇ = b₆ * b₅ & b₅ is continuous & b₆ is continuous holds
b₇ is continuous

proof end;

theorem Th11: :: JGRAPH_5:11

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Real
for b₉ being Function of (Closed-Interval-TSpace b₁,b₂),(Closed-Interval-TSpace b₃,b₄) st b₉ is_homeomorphism & b₉ . b₅ = b₇ & b₉ . b₆ = b₈ & b₉ . b₁ = b₃ & b₉ . b₂ = b₄ & b₃ <= b₄ & b₇ <= b₈ & b₅ in [.b₁,b₂.] & b₆ in [.b₁,b₂.] holds
b₅ <= b₆

proof end;

theorem Th12: :: JGRAPH_5:12

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Real
for b₉ being Function of (Closed-Interval-TSpace b₁,b₂),(Closed-Interval-TSpace b₃,b₄) st b₉ is_homeomorphism & b₉ . b₅ = b₇ & b₉ . b₆ = b₈ & b₉ . b₁ = b₄ & b₉ . b₂ = b₃ & b₄ >= b₃ & b₇ >= b₈ & b₅ in [.b₁,b₂.] & b₆ in [.b₁,b₂.] holds
b₅ <= b₆

proof end;

theorem Th13: :: JGRAPH_5:13

for b₁ being Nat holds - (0.REAL b₁) = 0.REAL b₁

proof end;

theorem Th14: :: JGRAPH_5:14

for b₁, b₂ being Function of I[01] ,(TOP-REAL 2)
for b₃, b₄, b₅, b₆ being Real
for b₇, b₈ being Point of I[01] st b₇ = 0 & b₈ = 1 & b₁ is continuous & b₁ is one-to-one & b₂ is continuous & b₂ is one-to-one & b₃ <> b₄ & b₅ <> b₆ & (b₁ . b₇) `1 = b₃ & b₅ <= (b₁ . b₇) `2 & (b₁ . b₇) `2 <= b₆ & (b₁ . b₈) `1 = b₄ & b₅ <= (b₁ . b₈) `2 & (b₁ . b₈) `2 <= b₆ & (b₂ . b₇) `2 = b₅ & b₃ <= (b₂ . b₇) `1 & (b₂ . b₇) `1 <= b₄ & (b₂ . b₈) `2 = b₆ & b₃ <= (b₂ . b₈) `1 & (b₂ . b₈) `1 <= b₄ & ( for b₉ being Point of I[01] holds
( ( b₃ >= (b₁ . b₉) `1 or (b₁ . b₉) `1 >= b₄ or b₅ >= (b₁ . b₉) `2 or (b₁ . b₉) `2 >= b₆ ) & ( b₃ >= (b₂ . b₉) `1 or (b₂ . b₉) `1 >= b₄ or b₅ >= (b₂ . b₉) `2 or (b₂ . b₉) `2 >= b₆ ) ) ) holds
rng b₁ meets rng b₂

proof end;

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

theorem Th15: :: JGRAPH_5:15

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

proof end;

theorem Th16: :: JGRAPH_5:16

for b₁, b₂ being Function of I[01] ,(TOP-REAL 2)
for b₃, b₄, b₅, b₆, b₇ being Subset of (TOP-REAL 2)
for b₈, b₉ being Point of I[01] st b₈ = 0 & b₉ = 1 & b₁ is continuous & b₁ is one-to-one & b₂ is continuous & b₂ is one-to-one & b₃ = { b₁₀ where B is Point of (TOP-REAL 2) : |.b₁₀.| <= 1 } & b₄ = { b₁₀ where B is Point of (TOP-REAL 2) : ( |.b₁₀.| = 1 & b₁₀ `2 <= b₁₀ `1 & b₁₀ `2 >= - (b₁₀ `1 ) ) } & b₅ = { b₁₀ where B is Point of (TOP-REAL 2) : ( |.b₁₀.| = 1 & b₁₀ `2 >= b₁₀ `1 & b₁₀ `2 <= - (b₁₀ `1 ) ) } & b₆ = { b₁₀ where B is Point of (TOP-REAL 2) : ( |.b₁₀.| = 1 & b₁₀ `2 >= b₁₀ `1 & b₁₀ `2 >= - (b₁₀ `1 ) ) } & b₇ = { b₁₀ where B is Point of (TOP-REAL 2) : ( |.b₁₀.| = 1 & b₁₀ `2 <= b₁₀ `1 & b₁₀ `2 <= - (b₁₀ `1 ) ) } & b₁ . b₈ in b₅ & b₁ . b₉ in b₄ & b₂ . b₈ in b₆ & b₂ . b₉ in b₇ & rng b₁ c= b₃ & rng b₂ c= b₃ holds
rng b₁ meets rng b₂

proof end;

theorem Th17: :: JGRAPH_5:17

for b₁, b₂ being Function of I[01] ,(TOP-REAL 2)
for b₃, b₄, b₅, b₆, b₇ being Subset of (TOP-REAL 2)
for b₈, b₉ being Point of I[01] st b₈ = 0 & b₉ = 1 & b₁ is continuous & b₁ is one-to-one & b₂ is continuous & b₂ is one-to-one & b₃ = { b₁₀ where B is Point of (TOP-REAL 2) : |.b₁₀.| >= 1 } & b₄ = { b₁₀ where B is Point of (TOP-REAL 2) : ( |.b₁₀.| = 1 & b₁₀ `2 <= b₁₀ `1 & b₁₀ `2 >= - (b₁₀ `1 ) ) } & b₅ = { b₁₀ where B is Point of (TOP-REAL 2) : ( |.b₁₀.| = 1 & b₁₀ `2 >= b₁₀ `1 & b₁₀ `2 <= - (b₁₀ `1 ) ) } & b₆ = { b₁₀ where B is Point of (TOP-REAL 2) : ( |.b₁₀.| = 1 & b₁₀ `2 >= b₁₀ `1 & b₁₀ `2 >= - (b₁₀ `1 ) ) } & b₇ = { b₁₀ where B is Point of (TOP-REAL 2) : ( |.b₁₀.| = 1 & b₁₀ `2 <= b₁₀ `1 & b₁₀ `2 <= - (b₁₀ `1 ) ) } & b₁ . b₈ in b₅ & b₁ . b₉ in b₄ & b₂ . b₈ in b₇ & b₂ . b₉ in b₆ & rng b₁ c= b₃ & rng b₂ c= b₃ holds
rng b₁ meets rng b₂

proof end;

theorem Th18: :: JGRAPH_5:18

for b₁, b₂ being Function of I[01] ,(TOP-REAL 2)
for b₃, b₄, b₅, b₆, b₇ being Subset of (TOP-REAL 2)
for b₈, b₉ being Point of I[01] st b₈ = 0 & b₉ = 1 & b₁ is continuous & b₁ is one-to-one & b₂ is continuous & b₂ is one-to-one & b₃ = { b₁₀ where B is Point of (TOP-REAL 2) : |.b₁₀.| >= 1 } & b₄ = { b₁₀ where B is Point of (TOP-REAL 2) : ( |.b₁₀.| = 1 & b₁₀ `2 <= b₁₀ `1 & b₁₀ `2 >= - (b₁₀ `1 ) ) } & b₅ = { b₁₀ where B is Point of (TOP-REAL 2) : ( |.b₁₀.| = 1 & b₁₀ `2 >= b₁₀ `1 & b₁₀ `2 <= - (b₁₀ `1 ) ) } & b₆ = { b₁₀ where B is Point of (TOP-REAL 2) : ( |.b₁₀.| = 1 & b₁₀ `2 >= b₁₀ `1 & b₁₀ `2 >= - (b₁₀ `1 ) ) } & b₇ = { b₁₀ where B is Point of (TOP-REAL 2) : ( |.b₁₀.| = 1 & b₁₀ `2 <= b₁₀ `1 & b₁₀ `2 <= - (b₁₀ `1 ) ) } & b₁ . b₈ in b₅ & b₁ . b₉ in b₄ & b₂ . b₈ in b₆ & b₂ . b₉ in b₇ & rng b₁ c= b₃ & rng b₂ c= b₃ holds
rng b₁ meets rng b₂

proof end;

theorem Th19: :: JGRAPH_5:19

for b₁, b₂ being Function of I[01] ,(TOP-REAL 2)
for b₃ being Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| >= 1 } & b₁ is continuous & b₁ is one-to-one & b₂ is continuous & b₂ is one-to-one & b₁ . 0 = |[(- 1),0]| & b₁ . 1 = |[1,0]| & b₂ . 1 = |[0,1]| & b₂ . 0 = |[0,(- 1)]| & rng b₁ c= b₃ & rng b₂ c= b₃ holds
rng b₁ meets rng b₂

proof end;

theorem Th20: :: JGRAPH_5:20

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being Subset of (TOP-REAL 2) st b₅ = { b₆ where B is Point of (TOP-REAL 2) : |.b₆.| >= 1 } & |.b₁.| = 1 & |.b₂.| = 1 & |.b₃.| = 1 & |.b₄.| = 1 & ex b₆ being Function of (TOP-REAL 2),(TOP-REAL 2) st
( b₆ is_homeomorphism & b₆ .: b₅ c= b₅ & b₆ . b₁ = |[(- 1),0]| & b₆ . b₂ = |[0,1]| & b₆ . b₃ = |[1,0]| & b₆ . b₄ = |[0,(- 1)]| ) holds
for b₆, b₇ being Function of I[01] ,(TOP-REAL 2) st b₆ is continuous & b₆ is one-to-one & b₇ is continuous & b₇ is one-to-one & b₆ . 0 = b₁ & b₆ . 1 = b₃ & b₇ . 0 = b₄ & b₇ . 1 = b₂ & rng b₆ c= b₅ & rng b₇ c= b₅ holds
rng b₆ meets rng b₇

proof end;

theorem Th21: :: JGRAPH_5:21

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 > 0 holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphN ) . b₂ holds
b₃ `2 > 0

proof end;

theorem Th22: :: JGRAPH_5:22

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 >= 0 holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphN ) . b₂ holds
b₃ `2 >= 0

proof end;

theorem Th23: :: JGRAPH_5:23

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 >= 0 & (b₂ `1 ) / |.b₂.| < b₁ & |.b₂.| <> 0 holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphN ) . b₂ holds
( b₃ `2 >= 0 & b₃ `1 < 0 )

proof end;

theorem Th24: :: JGRAPH_5:24

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 >= 0 & b₃ `2 >= 0 & |.b₂.| <> 0 & |.b₃.| <> 0 & (b₂ `1 ) / |.b₂.| < (b₃ `1 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphN ) . b₂ & b₅ = (b₁ -FanMorphN ) . b₃ holds
(b₄ `1 ) / |.b₄.| < (b₅ `1 ) / |.b₅.|

proof end;

theorem Th25: :: JGRAPH_5:25

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 > 0 holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphE ) . b₂ holds
b₃ `1 > 0

proof end;

theorem Th26: :: JGRAPH_5:26

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 >= 0 & (b₂ `2 ) / |.b₂.| < b₁ & |.b₂.| <> 0 holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphE ) . b₂ holds
( b₃ `1 >= 0 & b₃ `2 < 0 )

proof end;

theorem Th27: :: JGRAPH_5:27

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `1 >= 0 & b₃ `1 >= 0 & |.b₂.| <> 0 & |.b₃.| <> 0 & (b₂ `2 ) / |.b₂.| < (b₃ `2 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphE ) . b₂ & b₅ = (b₁ -FanMorphE ) . b₃ holds
(b₄ `2 ) / |.b₄.| < (b₅ `2 ) / |.b₅.|

proof end;

theorem Th28: :: JGRAPH_5:28

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 < 0 holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphS ) . b₂ holds
b₃ `2 < 0

proof end;

theorem Th29: :: JGRAPH_5:29

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 < 0 & (b₂ `1 ) / |.b₂.| > b₁ holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphS ) . b₂ holds
( b₃ `2 < 0 & b₃ `1 > 0 )

proof end;

theorem Th30: :: JGRAPH_5:30

for b₁ being Real
for b₂, b₃ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 <= 0 & b₃ `2 <= 0 & |.b₂.| <> 0 & |.b₃.| <> 0 & (b₂ `1 ) / |.b₂.| < (b₃ `1 ) / |.b₃.| holds
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ = (b₁ -FanMorphS ) . b₂ & b₅ = (b₁ -FanMorphS ) . b₃ holds
(b₄ `1 ) / |.b₄.| < (b₅ `1 ) / |.b₅.|

proof end;

E26: now

let c₁ be non empty compact Subset of (TOP-REAL 2);
assume E27: c₁ = { b₁ where B is Point of (TOP-REAL 2) : |.b₁.| = 1 } ;
E28: proj1 .: c₁ c= [.(- 1),1.]

proof

let c₂ be set ; :: according to TARSKI:def 3
assume c₂ in proj1 .: c₁ ;
then consider c₃ being set such that
E29: ( c₃ in dom proj1 & c₃ in c₁ & c₂ = proj1 . c₃ ) by FUNCT_1:def 12;
reconsider c₄ = c₃ as Point of (TOP-REAL 2) by E29;
E30: c₂ = c₄ `1 by E29, PSCOMP_1:def 28;
consider c₅ being Point of (TOP-REAL 2) such that
E31: ( c₅ = c₃ & |.c₅.| = 1 ) by E27, E29;
E32: ((c₄ `1 ) ^2 ) + ((c₄ `2 ) ^2 ) = 1 by E31, JGRAPH_3:10, SQUARE_1:59;
0 <= (c₄ `2 ) ^2 by SQUARE_1:72;
then (1 - ((c₄ `1 ) ^2 )) + ((c₄ `1 ) ^2 ) >= 0 + ((c₄ `1 ) ^2 ) by E32, XREAL_1:9;
then ( - 1 <= c₄ `1 & c₄ `1 <= 1 ) by JGRAPH_4:4;
hence c₂ in [.(- 1),1.] by E30, RCOMP_1:48;

end;

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

proof

let c₂ be set ; :: according to TARSKI:def 3
assume c₂ in [.(- 1),1.] ;
then c₂ in { b₁ where B is Real : ( - 1 <= b₁ & b₁ <= 1 ) } by RCOMP_1:def 1;
then consider c₃ being Real such that
E29: ( c₂ = c₃ & - 1 <= c₃ & c₃ <= 1 ) ;
set c₄ = |[c₃,(sqrt (1 - (c₃ ^2 )))]|;
E30: dom proj1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
E31: ( |[c₃,(sqrt (1 - (c₃ ^2 )))]| `1 = c₃ & |[c₃,(sqrt (1 - (c₃ ^2 )))]| `2 = sqrt (1 - (c₃ ^2 )) ) by EUCLID:56;
1 ^2 >= c₃ ^2 by E29, JGRAPH_2:7;
then E32: 1 - (c₃ ^2 ) >= 0 by XREAL_1:50, SQUARE_1:59;
|.|[c₃,(sqrt (1 - (c₃ ^2 )))]|.| = sqrt ((c₃ ^2 ) + ((sqrt (1 - (c₃ ^2 ))) ^2 )) by E31, JGRAPH_3:10
.= sqrt ((c₃ ^2 ) + (1 - (c₃ ^2 ))) by E32, SQUARE_1:def 4
.= 1 by SQUARE_1:83 ;
then E33: |[c₃,(sqrt (1 - (c₃ ^2 )))]| in c₁ by E27;
proj1 . |[c₃,(sqrt (1 - (c₃ ^2 )))]| = |[c₃,(sqrt (1 - (c₃ ^2 )))]| `1 by PSCOMP_1:def 28
.= c₃ by EUCLID:56 ;
hence c₂ in proj1 .: c₁ by E29, E30, E33, FUNCT_1:def 12;

end;

hence proj1 .: c₁ = [.(- 1),1.] by E28, XBOOLE_0:def 10;
E29: proj2 .: c₁ c= [.(- 1),1.]

proof

let c₂ be set ; :: according to TARSKI:def 3
assume c₂ in proj2 .: c₁ ;
then consider c₃ being set such that
E30: ( c₃ in dom proj2 & c₃ in c₁ & c₂ = proj2 . c₃ ) by FUNCT_1:def 12;
reconsider c₄ = c₃ as Point of (TOP-REAL 2) by E30;
E31: c₂ = c₄ `2 by E30, PSCOMP_1:def 29;
consider c₅ being Point of (TOP-REAL 2) such that
E32: ( c₅ = c₃ & |.c₅.| = 1 ) by E27, E30;
E33: ((c₄ `1 ) ^2 ) + ((c₄ `2 ) ^2 ) = 1 by E32, JGRAPH_3:10, SQUARE_1:59;
0 <= (c₄ `1 ) ^2 by SQUARE_1:72;
then (1 - ((c₄ `2 ) ^2 )) + ((c₄ `2 ) ^2 ) >= 0 + ((c₄ `2 ) ^2 ) by E33, XREAL_1:9;
then ( - 1 <= c₄ `2 & c₄ `2 <= 1 ) by JGRAPH_4:4;
hence c₂ in [.(- 1),1.] by E31, RCOMP_1:48;

end;

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

proof

let c₂ be set ; :: according to TARSKI:def 3
assume c₂ in [.(- 1),1.] ;
then c₂ in { b₁ where B is Real : ( - 1 <= b₁ & b₁ <= 1 ) } by RCOMP_1:def 1;
then consider c₃ being Real such that
E30: ( c₂ = c₃ & - 1 <= c₃ & c₃ <= 1 ) ;
set c₄ = |[(sqrt (1 - (c₃ ^2 ))),c₃]|;
E31: dom proj2 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
E32: ( |[(sqrt (1 - (c₃ ^2 ))),c₃]| `2 = c₃ & |[(sqrt (1 - (c₃ ^2 ))),c₃]| `1 = sqrt (1 - (c₃ ^2 )) ) by EUCLID:56;
1 ^2 >= c₃ ^2 by E30, JGRAPH_2:7;
then E33: 1 - (c₃ ^2 ) >= 0 by XREAL_1:50, SQUARE_1:59;
|.|[(sqrt (1 - (c₃ ^2 ))),c₃]|.| = sqrt (((sqrt (1 - (c₃ ^2 ))) ^2 ) + (c₃ ^2 )) by E32, JGRAPH_3:10
.= sqrt ((1 - (c₃ ^2 )) + (c₃ ^2 )) by E33, SQUARE_1:def 4
.= 1 by SQUARE_1:83 ;
then E34: |[(sqrt (1 - (c₃ ^2 ))),c₃]| in c₁ by E27;
proj2 . |[(sqrt (1 - (c₃ ^2 ))),c₃]| = |[(sqrt (1 - (c₃ ^2 ))),c₃]| `2 by PSCOMP_1:def 29
.= c₃ by EUCLID:56 ;
hence c₂ in proj2 .: c₁ by E30, E31, E34, FUNCT_1:def 12;

end;

hence proj2 .: c₁ = [.(- 1),1.] by E29, XBOOLE_0:def 10;

end;

Lemma27: for b₁ being non empty compact Subset of (TOP-REAL 2) st b₁ = { b₂ where B is Point of (TOP-REAL 2) : |.b₂.| = 1 } holds
W-bound b₁ = - 1

proof end;

theorem Th31: :: JGRAPH_5:31

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

proof end;

theorem Th32: :: JGRAPH_5:32

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

proof end;

theorem Th33: :: JGRAPH_5:33

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

proof end;

theorem Th34: :: JGRAPH_5:34

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

proof end;

theorem Th35: :: JGRAPH_5:35

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

proof end;

theorem Th36: :: JGRAPH_5:36

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

proof end;

theorem Th37: :: JGRAPH_5:37

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

proof end;

theorem Th38: :: JGRAPH_5:38

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

proof end;

theorem Th39: :: JGRAPH_5:39

for b₁, b₂, b₃, b₄ being Real st b₁ <= b₂ & b₄ > 0 holds
ex b₅ being Function of (Closed-Interval-TSpace b₁,b₂),(Closed-Interval-TSpace ((b₄ * b₁) + b₃),((b₄ * b₂) + b₃)) st
( b₅ is_homeomorphism & ( for b₆ being Real st b₆ in [.b₁,b₂.] holds
b₅ . b₆ = (b₄ * b₆) + b₃ ) )

proof end;

theorem Th40: :: JGRAPH_5:40

for b₁, b₂, b₃, b₄ being Real st b₁ <= b₂ & b₄ < 0 holds
ex b₅ being Function of (Closed-Interval-TSpace b₁,b₂),(Closed-Interval-TSpace ((b₄ * b₂) + b₃),((b₄ * b₁) + b₃)) st
( b₅ is_homeomorphism & ( for b₆ being Real st b₆ in [.b₁,b₂.] holds
b₅ . b₆ = (b₄ * b₆) + b₃ ) )

proof end;

theorem Th41: :: JGRAPH_5:41

ex b₁ being Function of I[01] ,(Closed-Interval-TSpace (- 1),1) st
( b₁ is_homeomorphism & ( for b₂ being Real st b₂ in [.0,1.] holds
b₁ . b₂ = ((- 2) * b₂) + 1 ) & b₁ . 0 = 1 & b₁ . 1 = - 1 )

proof end;

theorem Th42: :: JGRAPH_5:42

ex b₁ being Function of I[01] ,(Closed-Interval-TSpace (- 1),1) st
( b₁ is_homeomorphism & ( for b₂ being Real st b₂ in [.0,1.] holds
b₁ . b₂ = (2 * b₂) - 1 ) & b₁ . 0 = - 1 & b₁ . 1 = 1 )

proof end;

E39: now

let c₁ be non empty compact Subset of (TOP-REAL 2);
assume E40: c₁ = { b₁ where B is Point of (TOP-REAL 2) : |.b₁.| = 1 } ;
reconsider c₂ = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
set c₃ = Lower_Arc c₁;
reconsider c₄ = c₂ | (Lower_Arc c₁) as Function of ((TOP-REAL 2) | (Lower_Arc c₁)),R^1 by JGRAPH_3:12;
E41: for b₁ being Point of ((TOP-REAL 2) | (Lower_Arc c₁)) holds c₄ . b₁ = proj1 . b₁

proof

let c₅ be Point of ((TOP-REAL 2) | (Lower_Arc c₁));
c₅ in the carrier of ((TOP-REAL 2) | (Lower_Arc c₁)) ;
then c₅ in Lower_Arc c₁ by JORDAN1:1;
hence c₄ . c₅ = proj1 . c₅ by FUNCT_1:72;

end;

then E42: c₄ is continuous by JGRAPH_2:39;
E43: dom c₄ = the carrier of ((TOP-REAL 2) | (Lower_Arc c₁)) by FUNCT_2:def 1;
then E44: dom c₄ = Lower_Arc c₁ by JORDAN1:1;
E45: Lower_Arc c₁ c= c₁ by E40, Th36;
E46: rng c₄ c= the carrier of (Closed-Interval-TSpace (- 1),1)

proof

let c₅ be set ; :: according to TARSKI:def 3
assume c₅ in rng c₄ ;
then consider c₆ being set such that
E47: ( c₆ in dom c₄ & c₅ = c₄ . c₆ ) by FUNCT_1:def 5;
c₆ in c₁ by E44, E45, E47;
then consider c₇ being Point of (TOP-REAL 2) such that
E48: ( c₇ = c₆ & |.c₇.| = 1 ) by E40;
E49: c₅ = proj1 . c₇ by E41, E43, E47, E48
.= c₇ `1 by PSCOMP_1:def 28 ;
1 = ((c₇ `1 ) ^2 ) + ((c₇ `2 ) ^2 ) by E48, JGRAPH_3:10, SQUARE_1:59;
then 1 - ((c₇ `1 ) ^2 ) >= 0 by SQUARE_1:72;
then - (1 - ((c₇ `1 ) ^2 )) <= 0 by XREAL_1:60;
then ((c₇ `1 ) ^2 ) - 1 <= 0 ;
then ( - 1 <= c₇ `1 & c₇ `1 <= 1 ) by JGRAPH_3:5;
then c₅ in [.(- 1),1.] by E49, RCOMP_1:48;
hence c₅ in the carrier of (Closed-Interval-TSpace (- 1),1) by TOPMETR:25;

end;

then reconsider c₅ = c₄ as Function of ((TOP-REAL 2) | (Lower_Arc c₁)),(Closed-Interval-TSpace (- 1),1) by E43, FUNCT_2:4;
dom c₅ = the carrier of ((TOP-REAL 2) | (Lower_Arc c₁)) by FUNCT_2:def 1;
then dom c₅ = [#] ((TOP-REAL 2) | (Lower_Arc c₁)) by PRE_TOPC:12;
then E47: dom c₅ = Lower_Arc c₁ by PRE_TOPC:def 10;
E48: rng c₄ c= [#] (Closed-Interval-TSpace (- 1),1) by E46, PRE_TOPC:12;
E49: [#] (Closed-Interval-TSpace (- 1),1) c= rng c₅

proof

let c₆ be set ; :: according to TARSKI:def 3
assume c₆ in [#] (Closed-Interval-TSpace (- 1),1) ;
then c₆ in the carrier of (Closed-Interval-TSpace (- 1),1) ;
then E50: c₆ in [.(- 1),1.] by TOPMETR:25;
then reconsider c₇ = c₆ as Real ;
set c₈ = |[c₇,(- (sqrt (1 - (c₇ ^2 ))))]|;
E51: |.|[c₇,(- (sqrt (1 - (c₇ ^2 ))))]|.| = sqrt (((|[c₇,(- (sqrt (1 - (c₇ ^2 ))))]| `1 ) ^2 ) + ((|[c₇,(- (sqrt (1 - (c₇ ^2 ))))]| `2 ) ^2 )) by JGRAPH_3:10
.= sqrt ((c₇ ^2 ) + ((|[c₇,(- (sqrt (1 - (c₇ ^2 ))))]| `2 ) ^2 )) by EUCLID:56
.= sqrt ((c₇ ^2 ) + ((- (sqrt (1 - (c₇ ^2 )))) ^2 )) by EUCLID:56
.= sqrt ((c₇ ^2 ) + ((sqrt (1 - (c₇ ^2 ))) ^2 )) by SQUARE_1:61 ;
( - 1 <= c₇ & c₇ <= 1 ) by E50, RCOMP_1:48;
then 1 ^2 >= c₇ ^2 by JGRAPH_2:7;
then E52: 1 - (c₇ ^2 ) >= 0 by XREAL_1:50, SQUARE_1:59;
then 0 <= sqrt (1 - (c₇ ^2 )) by SQUARE_1:def 4;
then E53: - (sqrt (1 - (c₇ ^2 ))) <= 0 by XREAL_1:60;
|.|[c₇,(- (sqrt (1 - (c₇ ^2 ))))]|.| = sqrt ((c₇ ^2 ) + (1 - (c₇ ^2 ))) by E51, E52, SQUARE_1:def 4
.= 1 by SQUARE_1:83 ;
then E54: |[c₇,(- (sqrt (1 - (c₇ ^2 ))))]| in c₁ by E40;
|[c₇,(- (sqrt (1 - (c₇ ^2 ))))]| `2 = - (sqrt (1 - (c₇ ^2 ))) by EUCLID:56;
then |[c₇,(- (sqrt (1 - (c₇ ^2 ))))]| in { b₁ where B is Point of (TOP-REAL 2) : ( b₁ in c₁ & b₁ `2 <= 0 ) } by E53, E54;
then E55: |[c₇,(- (sqrt (1 - (c₇ ^2 ))))]| in dom c₅ by E40, E47, Th38;
then c₅ . |[c₇,(- (sqrt (1 - (c₇ ^2 ))))]| = proj1 . |[c₇,(- (sqrt (1 - (c₇ ^2 ))))]| by E41, E43
.= |[c₇,(- (sqrt (1 - (c₇ ^2 ))))]| `1 by PSCOMP_1:def 28
.= c₇ by EUCLID:56 ;
hence c₆ in rng c₅ by E55, FUNCT_1:def 5;

end;

reconsider c₆ = [.(- 1),1.] as non empty Subset of R^1 by TOPMETR:24, RCOMP_1:48;
E50: Closed-Interval-TSpace (- 1),1 = R^1 | c₆ by TOPMETR:26;
for b₁, b₂ being set st b₁ in dom c₅ & b₂ in dom c₅ & c₅ . b₁ = c₅ . b₂ holds
b₁ = b₂

proof

let c₇, c₈ be set ;
assume E51: ( c₇ in dom c₅ & c₈ in dom c₅ & c₅ . c₇ = c₅ . c₈ ) ;
then reconsider c₉ = c₇ as Point of (TOP-REAL 2) by E47;
reconsider c₁₀ = c₈ as Point of (TOP-REAL 2) by E47, E51;
E52: c₅ . c₇ = proj1 . c₉ by E41, E43, E51
.= c₉ `1 by PSCOMP_1:def 28 ;
E53: c₅ . c₈ = proj1 . c₁₀ by E41, E43, E51
.= c₁₀ `1 by PSCOMP_1:def 28 ;
E54: c₉ in c₁ by E45, E47, E51;
c₁₀ in c₁ by E45, E47, E51;
then consider c₁₁ being Point of (TOP-REAL 2) such that
E55: ( c₁₀ = c₁₁ & |.c₁₁.| = 1 ) by E40;
1 ^2 = ((c₁₀ `1 ) ^2 ) + ((c₁₀ `2 ) ^2 ) by E55, JGRAPH_3:10;
then E56: (1 ^2 ) - ((c₁₀ `1 ) ^2 ) = (c₁₀ `2 ) ^2 ;
consider c₁₂ being Point of (TOP-REAL 2) such that
E57: ( c₉ = c₁₂ & |.c₁₂.| = 1 ) by E40, E54;
1 ^2 = ((c₉ `1 ) ^2 ) + ((c₉ `2 ) ^2 ) by E57, JGRAPH_3:10;
then (1 ^2 ) - ((c₉ `1 ) ^2 ) = (c₉ `2 ) ^2 ;
then (- (c₉ `2 )) ^2 = (c₁₀ `2 ) ^2 by E51, E52, E53, E56, SQUARE_1:61;
then E58: (- (c₉ `2 )) ^2 = (- (c₁₀ `2 )) ^2 by SQUARE_1:61;
c₉ in { b₁ where B is Point of (TOP-REAL 2) : ( b₁ in c₁ & b₁ `2 <= 0 ) } by E40, E47, E51, Th38;
then consider c₁₃ being Point of (TOP-REAL 2) such that
E59: ( c₉ = c₁₃ & c₁₃ in c₁ & c₁₃ `2 <= 0 ) ;
- (- (c₉ `2 )) <= 0 by E59;
then - (c₉ `2 ) >= 0 by XREAL_1:60;
then E60: - (c₉ `2 ) = sqrt ((- (c₁₀ `2 )) ^2 ) by E58, SQUARE_1:89;
c₁₀ in { b₁ where B is Point of (TOP-REAL 2) : ( b₁ in c₁ & b₁ `2 <= 0 ) } by E40, E47, E51, Th38;
then consider c₁₄ being Point of (TOP-REAL 2) such that
E61: ( c₁₀ = c₁₄ & c₁₄ in c₁ & c₁₄ `2 <= 0 ) ;
- (- (c₁₀ `2 )) <= 0 by E61;
then - (c₁₀ `2 ) >= 0 by XREAL_1:60;
then - (c₉ `2 ) = - (c₁₀ `2 ) by E60, SQUARE_1:89;
then - (- (c₉ `2 )) = c₁₀ `2 ;
then c₉ = |[(c₁₀ `1 ),(c₁₀ `2 )]| by E51, E52, E53, EUCLID:57
.= c₁₀ by EUCLID:57 ;
hence c₇ = c₈ ;

end;

hence ( proj1 | (Lower_Arc c₁) is continuous Function of ((TOP-REAL 2) | (Lower_Arc c₁)),(Closed-Interval-TSpace (- 1),1) & proj1 | (Lower_Arc c₁) is one-to-one & rng (proj1 | (Lower_Arc c₁)) = [#] (Closed-Interval-TSpace (- 1),1) ) by E42, E48, E49, E50, FUNCT_1:def 8, JGRAPH_1:63, XBOOLE_0:def 10;

end;

E40: now

let c₁ be non empty compact Subset of (TOP-REAL 2);
assume E41: c₁ = { b₁ where B is Point of (TOP-REAL 2) : |.b₁.| = 1 } ;
reconsider c₂ = proj1 as Function of (TOP-REAL 2),R^1 by TOPMETR:24;
set c₃ = Upper_Arc c₁;
reconsider c₄ = c₂ | (Upper_Arc c₁) as Function of ((TOP-REAL 2) | (Upper_Arc c₁)),R^1 by JGRAPH_3:12;
E42: for b₁ being Point of ((TOP-REAL 2) | (Upper_Arc c₁)) holds c₄ . b₁ = proj1 . b₁

proof

let c₅ be Point of ((TOP-REAL 2) | (Upper_Arc c₁));
c₅ in the carrier of ((TOP-REAL 2) | (Upper_Arc c₁)) ;
then c₅ in Upper_Arc c₁ by JORDAN1:1;
hence c₄ . c₅ = proj1 . c₅ by FUNCT_1:72;

end;

then E43: c₄ is continuous by JGRAPH_2:39;
E44: dom c₄ = the carrier of ((TOP-REAL 2) | (Upper_Arc c₁)) by FUNCT_2:def 1;
then E45: dom c₄ = Upper_Arc c₁ by JORDAN1:1;
E46: Upper_Arc c₁ c= c₁ by E41, Th36;
E47: rng c₄ c= the carrier of (Closed-Interval-TSpace (- 1),1)

proof

let c₅ be set ; :: according to TARSKI:def 3
assume c₅ in rng c₄ ;
then consider c₆ being set such that
E48: ( c₆ in dom c₄ & c₅ = c₄ . c₆ ) by FUNCT_1:def 5;
c₆ in c₁ by E45, E46, E48;
then consider c₇ being Point of (TOP-REAL 2) such that
E49: ( c₇ = c₆ & |.c₇.| = 1 ) by E41;
E50: c₅ = proj1 . c₇ by E42, E44, E48, E49
.= c₇ `1 by PSCOMP_1:def 28 ;
1 = ((c₇ `1 ) ^2 ) + ((c₇ `2 ) ^2 ) by E49, JGRAPH_3:10, SQUARE_1:59;
then 1 - ((c₇ `1 ) ^2 ) >= 0 by SQUARE_1:72;
then - (1 - ((c₇ `1 ) ^2 )) <= 0 by XREAL_1:60;
then ((c₇ `1 ) ^2 ) - 1 <= 0 ;
then ( - 1 <= c₇ `1 & c₇ `1 <= 1 ) by JGRAPH_3:5;
then c₅ in [.(- 1),1.] by E50, RCOMP_1:48;
hence c₅ in the carrier of (Closed-Interval-TSpace (- 1),1) by TOPMETR:25;

end;

then reconsider c₅ = c₄ as Function of ((TOP-REAL 2) | (Upper_Arc c₁)),(Closed-Interval-TSpace (- 1),1) by E44, FUNCT_2:4;
dom c₅ = the carrier of ((TOP-REAL 2) | (Upper_Arc c₁)) by FUNCT_2:def 1;
then dom c₅ = [#] ((TOP-REAL 2) | (Upper_Arc c₁)) by PRE_TOPC:12;
then E48: dom c₅ = Upper_Arc c₁ by PRE_TOPC:def 10;
E49: rng c₄ c= [#] (Closed-Interval-TSpace (- 1),1) by E47, PRE_TOPC:12;
E50: [#] (Closed-Interval-TSpace (- 1),1) c= rng c₅

proof

let c₆ be set ; :: according to TARSKI:def 3
assume c₆ in [#] (Closed-Interval-TSpace (- 1),1) ;
then c₆ in the carrier of (Closed-Interval-TSpace (- 1),1) ;
then E51: c₆ in [.(- 1),1.] by TOPMETR:25;
then reconsider c₇ = c₆ as Real ;
set c₈ = |[c₇,(sqrt (1 - (c₇ ^2 )))]|;
E52: |.|[c₇,(sqrt (1 - (c₇ ^2 )))]|.| = sqrt (((|[c₇,(sqrt (1 - (c₇ ^2 )))]| `1 ) ^2 ) + ((|[c₇,(sqrt (1 - (c₇ ^2 )))]| `2 ) ^2 )) by JGRAPH_3:10
.= sqrt ((c₇ ^2 ) + ((|[c₇,(sqrt (1 - (c₇ ^2 )))]| `2 ) ^2 )) by EUCLID:56
.= sqrt ((c₇ ^2 ) + ((sqrt (1 - (c₇ ^2 ))) ^2 )) by EUCLID:56 ;
( - 1 <= c₇ & c₇ <= 1 ) by E51, RCOMP_1:48;
then 1 ^2 >= c₇ ^2 by JGRAPH_2:7;
then E53: 1 - (c₇ ^2 ) >= 0 by XREAL_1:50, SQUARE_1:59;
then E54: 0 <= sqrt (1 - (c₇ ^2 )) by SQUARE_1:def 4;
|.|[c₇,(sqrt (1 - (c₇ ^2 )))]|.| = sqrt ((c₇ ^2 ) + (1 - (c₇ ^2 ))) by E52, E53, SQUARE_1:def 4
.= 1 by SQUARE_1:83 ;
then E55: |[c₇,(sqrt (1 - (c₇ ^2 )))]| in c₁ by E41;
|[c₇,(sqrt (1 - (c₇ ^2 )))]| `2 = sqrt (1 - (c₇ ^2 )) by EUCLID:56;
then |[c₇,(sqrt (1 - (c₇ ^2 )))]| in { b₁ where B is Point of (TOP-REAL 2) : ( b₁ in c₁ & b₁ `2 >= 0 ) } by E54, E55;
then E56: |[c₇,(sqrt (1 - (c₇ ^2 )))]| in dom c₅ by E41, E48, Th37;
then c₅ . |[c₇,(sqrt (1 - (c₇ ^2 )))]| = proj1 . |[c₇,(sqrt (1 - (c₇ ^2 )))]| by E42, E44
.= |[c₇,(sqrt (1 - (c₇ ^2 )))]| `1 by PSCOMP_1:def 28
.= c₇ by EUCLID:56 ;
hence c₆ in rng c₅ by E56, FUNCT_1:def 5;

end;

reconsider c₆ = [.(- 1),1.] as non empty Subset of R^1 by TOPMETR:24, RCOMP_1:48;
E51: Closed-Interval-TSpace (- 1),1 = R^1 | c₆ by TOPMETR:26;
for b₁, b₂ being set st b₁ in dom c₅ & b₂ in dom c₅ & c₅ . b₁ = c₅ . b₂ holds
b₁ = b₂

proof

let c₇, c₈ be set ;
assume E52: ( c₇ in dom c₅ & c₈ in dom c₅ & c₅ . c₇ = c₅ . c₈ ) ;
then reconsider c₉ = c₇ as Point of (TOP-REAL 2) by E48;
reconsider c₁₀ = c₈ as Point of (TOP-REAL 2) by E48, E52;
E53: c₅ . c₇ = proj1 . c₉ by E42, E44, E52
.= c₉ `1 by PSCOMP_1:def 28 ;
E54: c₅ . c₈ = proj1 . c₁₀ by E42, E44, E52
.= c₁₀ `1 by PSCOMP_1:def 28 ;
E55: c₉ in c₁ by E46, E48, E52;
c₁₀ in c₁ by E46, E48, E52;
then consider c₁₁ being Point of (TOP-REAL 2) such that
E56: ( c₁₀ = c₁₁ & |.c₁₁.| = 1 ) by E41;
1 ^2 = ((c₁₀ `1 ) ^2 ) + ((c₁₀ `2 ) ^2 ) by E56, JGRAPH_3:10;
then E57: (1 ^2 ) - ((c₁₀ `1 ) ^2 ) = (c₁₀ `2 ) ^2 ;
consider c₁₂ being Point of (TOP-REAL 2) such that
E58: ( c₉ = c₁₂ & |.c₁₂.| = 1 ) by E41, E55;
1 ^2 = ((c₉ `1 ) ^2 ) + ((c₉ `2 ) ^2 ) by E58, JGRAPH_3:10;
then E59: (c₉ `2 ) ^2 = (c₁₀ `2 ) ^2 by E52, E53, E54, E57, XCMPLX_1:26;
c₉ in { b₁ where B is Point of (TOP-REAL 2) : ( b₁ in c₁ & b₁ `2 >= 0 ) } by E41, E48, E52, Th37;
then consider c₁₃ being Point of (TOP-REAL 2) such that
E60: ( c₉ = c₁₃ & c₁₃ in c₁ & c₁₃ `2 >= 0 ) ;
E61: c₉ `2 = sqrt ((c₁₀ `2 ) ^2 ) by E59, E60, SQUARE_1:89;
c₁₀ in { b₁ where B is Point of (TOP-REAL 2) : ( b₁ in c₁ & b₁ `2 >= 0 ) } by E41, E48, E52, Th37;
then consider c₁₄ being Point of (TOP-REAL 2) such that
E62: ( c₁₀ = c₁₄ & c₁₄ in c₁ & c₁₄ `2 >= 0 ) ;
c₉ `2 = c₁₀ `2 by E61, E62, SQUARE_1:89;
then c₉ = |[(c₁₀ `1 ),(c₁₀ `2 )]| by E52, E53, E54, EUCLID:57
.= c₁₀ by EUCLID:57 ;
hence c₇ = c₈ ;

end;

hence ( proj1 | (Upper_Arc c₁) is continuous Function of ((TOP-REAL 2) | (Upper_Arc c₁)),(Closed-Interval-TSpace (- 1),1) & proj1 | (Upper_Arc c₁) is one-to-one & rng (proj1 | (Upper_Arc c₁)) = [#] (Closed-Interval-TSpace (- 1),1) ) by E43, E49, E50, E51, FUNCT_1:def 8, JGRAPH_1:63, XBOOLE_0:def 10;

end;

theorem Th43: :: JGRAPH_5:43

for b₁ being non empty compact Subset of (TOP-REAL 2) st b₁ = { b₂ where B is Point of (TOP-REAL 2) : |.b₂.| = 1 } holds
ex b₂ being Function of (Closed-Interval-TSpace (- 1),1),((TOP-REAL 2) | (Lower_Arc b₁)) st
( b₂ is_homeomorphism & ( for b₃ being Point of (TOP-REAL 2) st b₃ in Lower_Arc b₁ holds
b₂ . (b₃ `1 ) = b₃ ) & b₂ . (- 1) = W-min b₁ & b₂ . 1 = E-max b₁ )

proof end;

theorem Th44: :: JGRAPH_5:44

for b₁ being non empty compact Subset of (TOP-REAL 2) st b₁ = { b₂ where B is Point of (TOP-REAL 2) : |.b₂.| = 1 } holds
ex b₂ being Function of (Closed-Interval-TSpace (- 1),1),((TOP-REAL 2) | (Upper_Arc b₁)) st
( b₂ is_homeomorphism & ( for b₃ being Point of (TOP-REAL 2) st b₃ in Upper_Arc b₁ holds
b₂ . (b₃ `1 ) = b₃ ) & b₂ . (- 1) = W-min b₁ & b₂ . 1 = E-max b₁ )

proof end;

theorem Th45: :: JGRAPH_5:45

for b₁ being non empty compact Subset of (TOP-REAL 2) st b₁ = { b₂ where B is Point of (TOP-REAL 2) : |.b₂.| = 1 } holds
ex b₂ being Function of I[01] ,((TOP-REAL 2) | (Lower_Arc b₁)) st
( b₂ is_homeomorphism & ( for b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆ being Real st b₂ . b₅ = b₃ & b₂ . b₆ = b₄ & b₅ in [.0,1.] & b₆ in [.0,1.] holds
( b₅ < b₆ iff b₃ `1 > b₄ `1 ) ) & b₂ . 0 = E-max b₁ & b₂ . 1 = W-min b₁ )

proof end;

theorem Th46: :: JGRAPH_5:46

for b₁ being non empty compact Subset of (TOP-REAL 2) st b₁ = { b₂ where B is Point of (TOP-REAL 2) : |.b₂.| = 1 } holds
ex b₂ being Function of I[01] ,((TOP-REAL 2) | (Upper_Arc b₁)) st
( b₂ is_homeomorphism & ( for b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆ being Real st b₂ . b₅ = b₃ & b₂ . b₆ = b₄ & b₅ in [.0,1.] & b₆ in [.0,1.] holds
( b₅ < b₆ iff b₃ `1 < b₄ `1 ) ) & b₂ . 0 = W-min b₁ & b₂ . 1 = E-max b₁ )

proof end;

theorem Th47: :: JGRAPH_5:47

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| = 1 } & b₂ in Upper_Arc b₃ & LE b₁,b₂,b₃ holds
b₁ in Upper_Arc b₃

proof end;

theorem Th48: :: JGRAPH_5:48

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| = 1 } & LE b₁,b₂,b₃ & b₁ <> b₂ & b₁ `1 < 0 & b₂ `1 < 0 & b₁ `2 < 0 & b₂ `2 < 0 holds
( b₁ `1 > b₂ `1 & b₁ `2 < b₂ `2 )

proof end;

theorem Th49: :: JGRAPH_5:49

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| = 1 } & LE b₁,b₂,b₃ & b₁ <> b₂ & b₁ `1 < 0 & b₂ `1 < 0 & b₁ `2 >= 0 & b₂ `2 >= 0 holds
( b₁ `1 < b₂ `1 & b₁ `2 < b₂ `2 )

proof end;

theorem Th50: :: JGRAPH_5:50

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| = 1 } & LE b₁,b₂,b₃ & b₁ <> b₂ & b₁ `2 >= 0 & b₂ `2 >= 0 holds
b₁ `1 < b₂ `1

proof end;

theorem Th51: :: JGRAPH_5:51

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| = 1 } & LE b₁,b₂,b₃ & b₁ <> b₂ & b₁ `2 <= 0 & b₂ `2 <= 0 & b₁ <> W-min b₃ holds
b₁ `1 > b₂ `1

proof end;

theorem Th52: :: JGRAPH_5:52

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| = 1 } & ( b₂ `2 >= 0 or b₂ `1 >= 0 ) & LE b₁,b₂,b₃ & not b₁ `2 >= 0 holds
b₁ `1 >= 0

proof end;

theorem Th53: :: JGRAPH_5:53

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| = 1 } & LE b₁,b₂,b₃ & b₁ <> b₂ & b₁ `1 >= 0 & b₂ `1 >= 0 holds
b₁ `2 > b₂ `2

proof end;

theorem Th54: :: JGRAPH_5:54

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| = 1 } & b₁ in b₃ & b₂ in b₃ & b₁ `1 < 0 & b₂ `1 < 0 & b₁ `2 < 0 & b₂ `2 < 0 & ( b₁ `1 >= b₂ `1 or b₁ `2 <= b₂ `2 ) holds
LE b₁,b₂,b₃

proof end;

theorem Th55: :: JGRAPH_5:55

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| = 1 } & b₁ in b₃ & b₂ in b₃ & b₁ `1 > 0 & b₂ `1 > 0 & b₁ `2 < 0 & b₂ `2 < 0 & ( b₁ `1 >= b₂ `1 or b₁ `2 >= b₂ `2 ) holds
LE b₁,b₂,b₃

proof end;

theorem Th56: :: JGRAPH_5:56

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| = 1 } & b₁ in b₃ & b₂ in b₃ & b₁ `1 < 0 & b₂ `1 < 0 & b₁ `2 >= 0 & b₂ `2 >= 0 & ( b₁ `1 <= b₂ `1 or b₁ `2 <= b₂ `2 ) holds
LE b₁,b₂,b₃

proof end;

theorem Th57: :: JGRAPH_5:57

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| = 1 } & b₁ in b₃ & b₂ in b₃ & b₁ `2 >= 0 & b₂ `2 >= 0 & b₁ `1 <= b₂ `1 holds
LE b₁,b₂,b₃

proof end;

theorem Th58: :: JGRAPH_5:58

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| = 1 } & b₁ in b₃ & b₂ in b₃ & b₁ `1 >= 0 & b₂ `1 >= 0 & b₁ `2 >= b₂ `2 holds
LE b₁,b₂,b₃

proof end;

theorem Th59: :: JGRAPH_5:59

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ = { b₄ where B is Point of (TOP-REAL 2) : |.b₄.| = 1 } & b₁ in b₃ & b₂ in b₃ & b₁ `2 <= 0 & b₂ `2 <= 0 & b₂ <> W-min b₃ & b₁ `1 >= b₂ `1 holds
LE b₁,b₂,b₃

proof end;

theorem Th60: :: JGRAPH_5:60

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₂ `2 <= 0 holds
for b₃ being Point of (TOP-REAL 2) st b₃ = (b₁ -FanMorphS ) . b₂ holds
b₃ `2 <= 0

proof end;

theorem Th61: :: JGRAPH_5:61

for b₁ being Real
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL 2)
for b₆ being non empty compact Subset of (TOP-REAL 2) st - 1 < b₁ & b₁ < 1 & b₆ = { b₇ where B is Point of (TOP-REAL 2) : |.b₇.| = 1 } & LE b₂,b₃,b₆ & b₄ = (b₁ -FanMorphS ) . b₂ & b₅ = (b₁ -FanMorphS ) . b₃ holds
LE b₄,b₅,b₆

proof end;

theorem Th62: :: JGRAPH_5:62

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2) st b₅ = { b₆ where B is Point of (TOP-REAL 2) : |.b₆.| = 1 } & LE b₁,b₂,b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ & b₁ `1 < 0 & b₁ `2 >= 0 & b₂ `1 < 0 & b₂ `2 >= 0 & b₃ `1 < 0 & b₃ `2 >= 0 & b₄ `1 < 0 & b₄ `2 >= 0 holds
ex b₆ being Function of (TOP-REAL 2),(TOP-REAL 2)ex b₇, b₈, b₉, b₁₀ being Point of (TOP-REAL 2) st
( b₆ is_homeomorphism & ( for b₁₁ being Point of (TOP-REAL 2) holds |.(b₆ . b₁₁).| = |.b₁₁.| ) & b₇ = b₆ . b₁ & b₈ = b₆ . b₂ & b₉ = b₆ . b₃ & b₁₀ = b₆ . b₄ & b₇ `1 < 0 & b₇ `2 < 0 & b₈ `1 < 0 & b₈ `2 < 0 & b₉ `1 < 0 & b₉ `2 < 0 & b₁₀ `1 < 0 & b₁₀ `2 < 0 & LE b₇,b₈,b₅ & LE b₈,b₉,b₅ & LE b₉,b₁₀,b₅ )

proof end;

theorem Th63: :: JGRAPH_5:63

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2) st b₅ = { b₆ where B is Point of (TOP-REAL 2) : |.b₆.| = 1 } & LE b₁,b₂,b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ & b₁ `2 >= 0 & b₂ `2 >= 0 & b₃ `2 >= 0 & b₄ `2 > 0 holds
ex b₆ being Function of (TOP-REAL 2),(TOP-REAL 2)ex b₇, b₈, b₉, b₁₀ being Point of (TOP-REAL 2) st
( b₆ is_homeomorphism & ( for b₁₁ being Point of (TOP-REAL 2) holds |.(b₆ . b₁₁).| = |.b₁₁.| ) & b₇ = b₆ . b₁ & b₈ = b₆ . b₂ & b₉ = b₆ . b₃ & b₁₀ = b₆ . b₄ & b₇ `1 < 0 & b₇ `2 >= 0 & b₈ `1 < 0 & b₈ `2 >= 0 & b₉ `1 < 0 & b₉ `2 >= 0 & b₁₀ `1 < 0 & b₁₀ `2 >= 0 & LE b₇,b₈,b₅ & LE b₈,b₉,b₅ & LE b₉,b₁₀,b₅ )

proof end;

theorem Th64: :: JGRAPH_5:64

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2) st b₅ = { b₆ where B is Point of (TOP-REAL 2) : |.b₆.| = 1 } & LE b₁,b₂,b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ & b₁ `2 >= 0 & b₂ `2 >= 0 & b₃ `2 >= 0 & b₄ `2 > 0 holds
ex b₆ being Function of (TOP-REAL 2),(TOP-REAL 2)ex b₇, b₈, b₉, b₁₀ being Point of (TOP-REAL 2) st
( b₆ is_homeomorphism & ( for b₁₁ being Point of (TOP-REAL 2) holds |.(b₆ . b₁₁).| = |.b₁₁.| ) & b₇ = b₆ . b₁ & b₈ = b₆ . b₂ & b₉ = b₆ . b₃ & b₁₀ = b₆ . b₄ & b₇ `1 < 0 & b₇ `2 < 0 & b₈ `1 < 0 & b₈ `2 < 0 & b₉ `1 < 0 & b₉ `2 < 0 & b₁₀ `1 < 0 & b₁₀ `2 < 0 & LE b₇,b₈,b₅ & LE b₈,b₉,b₅ & LE b₉,b₁₀,b₅ )

proof end;

theorem Th65: :: JGRAPH_5:65

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2) st b₅ = { b₆ where B is Point of (TOP-REAL 2) : |.b₆.| = 1 } & LE b₁,b₂,b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ & ( b₁ `2 >= 0 or b₁ `1 >= 0 ) & ( b₂ `2 >= 0 or b₂ `1 >= 0 ) & ( b₃ `2 >= 0 or b₃ `1 >= 0 ) & ( b₄ `2 > 0 or b₄ `1 > 0 ) holds
ex b₆ being Function of (TOP-REAL 2),(TOP-REAL 2)ex b₇, b₈, b₉, b₁₀ being Point of (TOP-REAL 2) st
( b₆ is_homeomorphism & ( for b₁₁ being Point of (TOP-REAL 2) holds |.(b₆ . b₁₁).| = |.b₁₁.| ) & b₇ = b₆ . b₁ & b₈ = b₆ . b₂ & b₉ = b₆ . b₃ & b₁₀ = b₆ . b₄ & b₇ `2 >= 0 & b₈ `2 >= 0 & b₉ `2 >= 0 & b₁₀ `2 > 0 & LE b₇,b₈,b₅ & LE b₈,b₉,b₅ & LE b₉,b₁₀,b₅ )

proof end;

theorem Th66: :: JGRAPH_5:66

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2) st b₅ = { b₆ where B is Point of (TOP-REAL 2) : |.b₆.| = 1 } & LE b₁,b₂,b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ & ( b₁ `2 >= 0 or b₁ `1 >= 0 ) & ( b₂ `2 >= 0 or b₂ `1 >= 0 ) & ( b₃ `2 >= 0 or b₃ `1 >= 0 ) & ( b₄ `2 > 0 or b₄ `1 > 0 ) holds
ex b₆ being Function of (TOP-REAL 2),(TOP-REAL 2)ex b₇, b₈, b₉, b₁₀ being Point of (TOP-REAL 2) st
( b₆ is_homeomorphism & ( for b₁₁ being Point of (TOP-REAL 2) holds |.(b₆ . b₁₁).| = |.b₁₁.| ) & b₇ = b₆ . b₁ & b₈ = b₆ . b₂ & b₉ = b₆ . b₃ & b₁₀ = b₆ . b₄ & b₇ `1 < 0 & b₇ `2 < 0 & b₈ `1 < 0 & b₈ `2 < 0 & b₉ `1 < 0 & b₉ `2 < 0 & b₁₀ `1 < 0 & b₁₀ `2 < 0 & LE b₇,b₈,b₅ & LE b₈,b₉,b₅ & LE b₉,b₁₀,b₅ )

proof end;

theorem Th67: :: JGRAPH_5:67

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2) st b₅ = { b₆ where B is Point of (TOP-REAL 2) : |.b₆.| = 1 } & b₄ = W-min b₅ & LE b₁,b₂,b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ holds
ex b₆ being Function of (TOP-REAL 2),(TOP-REAL 2)ex b₇, b₈, b₉, b₁₀ being Point of (TOP-REAL 2) st
( b₆ is_homeomorphism & ( for b₁₁ being Point of (TOP-REAL 2) holds |.(b₆ . b₁₁).| = |.b₁₁.| ) & b₇ = b₆ . b₁ & b₈ = b₆ . b₂ & b₉ = b₆ . b₃ & b₁₀ = b₆ . b₄ & b₇ `1 < 0 & b₇ `2 < 0 & b₈ `1 < 0 & b₈ `2 < 0 & b₉ `1 < 0 & b₉ `2 < 0 & b₁₀ `1 < 0 & b₁₀ `2 < 0 & LE b₇,b₈,b₅ & LE b₈,b₉,b₅ & LE b₉,b₁₀,b₅ )

proof end;

theorem Th68: :: JGRAPH_5:68

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2) st b₅ = { b₆ where B is Point of (TOP-REAL 2) : |.b₆.| = 1 } & LE b₁,b₂,b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ holds
ex b₆ being Function of (TOP-REAL 2),(TOP-REAL 2)ex b₇, b₈, b₉, b₁₀ being Point of (TOP-REAL 2) st
( b₆ is_homeomorphism & ( for b₁₁ being Point of (TOP-REAL 2) holds |.(b₆ . b₁₁).| = |.b₁₁.| ) & b₇ = b₆ . b₁ & b₈ = b₆ . b₂ & b₉ = b₆ . b₃ & b₁₀ = b₆ . b₄ & b₇ `1 < 0 & b₇ `2 < 0 & b₈ `1 < 0 & b₈ `2 < 0 & b₉ `1 < 0 & b₉ `2 < 0 & b₁₀ `1 < 0 & b₁₀ `2 < 0 & LE b₇,b₈,b₅ & LE b₈,b₉,b₅ & LE b₉,b₁₀,b₅ )

proof end;

theorem Th69: :: JGRAPH_5:69

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2) st b₅ = { b₆ where B is Point of (TOP-REAL 2) : |.b₆.| = 1 } & LE b₁,b₂,b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ & b₁ <> b₂ & b₂ <> b₃ & b₃ <> b₄ & b₁ `1 < 0 & b₂ `1 < 0 & b₃ `1 < 0 & b₄ `1 < 0 & b₁ `2 < 0 & b₂ `2 < 0 & b₃ `2 < 0 & b₄ `2 < 0 holds
ex b₆ being Function of (TOP-REAL 2),(TOP-REAL 2) st
( b₆ is_homeomorphism & ( for b₇ being Point of (TOP-REAL 2) holds |.(b₆ . b₇).| = |.b₇.| ) & |[(- 1),0]| = b₆ . b₁ & |[0,1]| = b₆ . b₂ & |[1,0]| = b₆ . b₃ & |[0,(- 1)]| = b₆ . b₄ )

proof end;

theorem Th70: :: JGRAPH_5:70

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2) st b₅ = { b₆ where B is Point of (TOP-REAL 2) : |.b₆.| = 1 } & LE b₁,b₂,b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ & b₁ <> b₂ & b₂ <> b₃ & b₃ <> b₄ holds
ex b₆ being Function of (TOP-REAL 2),(TOP-REAL 2) st
( b₆ is_homeomorphism & ( for b₇ being Point of (TOP-REAL 2) holds |.(b₆ . b₇).| = |.b₇.| ) & |[(- 1),0]| = b₆ . b₁ & |[0,1]| = b₆ . b₂ & |[1,0]| = b₆ . b₃ & |[0,(- 1)]| = b₆ . b₄ )

proof end;

Lemma67: ( |[(- 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;

E68: now

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

end;

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

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

theorem Th71: :: JGRAPH_5:71

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2)
for b₆ being Subset of (TOP-REAL 2) st b₅ = { b₇ where B is Point of (TOP-REAL 2) : |.b₇.| = 1 } & LE b₁,b₂,b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ holds
for b₇, b₈ being Function of I[01] ,(TOP-REAL 2) st b₇ is continuous & b₇ is one-to-one & b₈ is continuous & b₈ is one-to-one & b₆ = { b₉ where B is Point of (TOP-REAL 2) : |.b₉.| <= 1 } & b₇ . 0 = b₁ & b₇ . 1 = b₃ & b₈ . 0 = b₂ & b₈ . 1 = b₄ & rng b₇ c= b₆ & rng b₈ c= b₆ holds
rng b₇ meets rng b₈

proof end;

theorem Th72: :: JGRAPH_5:72

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2)
for b₆ being Subset of (TOP-REAL 2) st b₅ = { b₇ where B is Point of (TOP-REAL 2) : |.b₇.| = 1 } & LE b₁,b₂,b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ holds
for b₇, b₈ being Function of I[01] ,(TOP-REAL 2) st b₇ is continuous & b₇ is one-to-one & b₈ is continuous & b₈ is one-to-one & b₆ = { b₉ where B is Point of (TOP-REAL 2) : |.b₉.| <= 1 } & b₇ . 0 = b₁ & b₇ . 1 = b₃ & b₈ . 0 = b₄ & b₈ . 1 = b₂ & rng b₇ c= b₆ & rng b₈ c= b₆ holds
rng b₇ meets rng b₈

proof end;

theorem Th73: :: JGRAPH_5:73

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2)
for b₆ being Subset of (TOP-REAL 2) st b₅ = { b₇ where B is Point of (TOP-REAL 2) : |.b₇.| = 1 } & LE b₁,b₂,b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ holds
for b₇, b₈ being Function of I[01] ,(TOP-REAL 2) st b₇ is continuous & b₇ is one-to-one & b₈ is continuous & b₈ is one-to-one & b₆ = { b₉ where B is Point of (TOP-REAL 2) : |.b₉.| >= 1 } & b₇ . 0 = b₁ & b₇ . 1 = b₃ & b₈ . 0 = b₄ & b₈ . 1 = b₂ & rng b₇ c= b₆ & rng b₈ c= b₆ holds
rng b₇ meets rng b₈

proof end;

theorem Th74: :: JGRAPH_5:74

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2)
for b₆ being Subset of (TOP-REAL 2) st b₅ = { b₇ where B is Point of (TOP-REAL 2) : |.b₇.| = 1 } & LE b₁,b₂,b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ holds
for b₇, b₈ being Function of I[01] ,(TOP-REAL 2) st b₇ is continuous & b₇ is one-to-one & b₈ is continuous & b₈ is one-to-one & b₆ = { b₉ where B is Point of (TOP-REAL 2) : |.b₉.| >= 1 } & b₇ . 0 = b₁ & b₇ . 1 = b₃ & b₈ . 0 = b₂ & b₈ . 1 = b₄ & rng b₇ c= b₆ & rng b₈ c= b₆ holds
rng b₇ meets rng b₈

proof end;