:: JGRAPH_6 semantic presentation

theorem Th1: :: JGRAPH_6:1

canceled;

theorem Th2: :: JGRAPH_6:2

for b₁, b₂, b₃ being real number st 0 <= b₃ & b₃ <= 1 & b₁ <= b₂ holds
( b₁ <= ((1 - b₃) * b₁) + (b₃ * b₂) & ((1 - b₃) * b₁) + (b₃ * b₂) <= b₂ ) by XREAL_1:174, XREAL_1:175;

Lemma2: for b₁, b₂ being real number st ( ( b₁ >= 0 & b₂ > 0 ) or ( b₁ > 0 & b₂ >= 0 ) ) holds
b₁ + b₂ > 0
by XREAL_1:36;

theorem Th3: :: JGRAPH_6:3

canceled;

theorem Th4: :: JGRAPH_6:4

for b₁, b₂ being real number st - 1 <= b₁ & b₁ <= 1 & - 1 <= b₂ & b₂ <= 1 holds
(b₁ ^2 ) * (b₂ ^2 ) <= 1

proof end;

theorem Th5: :: JGRAPH_6:5

for b₁, b₂ being real number st b₁ >= 0 & b₂ >= 0 holds
b₁ * (sqrt b₂) = sqrt ((b₁ ^2 ) * b₂)

proof end;

Lemma5: for b₁, b₂ being real number st - 1 <= b₁ & b₁ <= 1 & - 1 <= b₂ & b₂ <= 1 holds
(1 + (b₁ ^2 )) * (b₂ ^2 ) <= 1 + (b₂ ^2 )

proof end;

theorem Th6: :: JGRAPH_6:6

for b₁, b₂ being real number st - 1 <= b₁ & b₁ <= 1 & - 1 <= b₂ & b₂ <= 1 holds
( (- b₂) * (sqrt (1 + (b₁ ^2 ))) <= sqrt (1 + (b₂ ^2 )) & - (sqrt (1 + (b₂ ^2 ))) <= b₂ * (sqrt (1 + (b₁ ^2 ))) )

proof end;

theorem Th7: :: JGRAPH_6:7

for b₁, b₂ being real number st - 1 <= b₁ & b₁ <= 1 & - 1 <= b₂ & b₂ <= 1 holds
b₂ * (sqrt (1 + (b₁ ^2 ))) <= sqrt (1 + (b₂ ^2 ))

proof end;

Lemma8: for b₁, b₂ being real number st b₂ <= 0 & b₁ <= b₂ holds
b₁ * (sqrt (1 + (b₂ ^2 ))) <= b₂ * (sqrt (1 + (b₁ ^2 )))

proof end;

Lemma9: for b₁, b₂ being real number st b₁ <= 0 & b₁ <= b₂ holds
b₁ * (sqrt (1 + (b₂ ^2 ))) <= b₂ * (sqrt (1 + (b₁ ^2 )))

proof end;

Lemma10: for b₁, b₂ being real number st b₁ >= 0 & b₁ >= b₂ holds
b₁ * (sqrt (1 + (b₂ ^2 ))) >= b₂ * (sqrt (1 + (b₁ ^2 )))

proof end;

theorem Th8: :: JGRAPH_6:8

for b₁, b₂ being real number st b₁ >= b₂ holds
b₁ * (sqrt (1 + (b₂ ^2 ))) >= b₂ * (sqrt (1 + (b₁ ^2 )))

proof end;

theorem Th9: :: JGRAPH_6:9

for b₁, b₂, b₃ being real number
for b₄ being Point of (TOP-REAL 2) st b₂ <= b₃ & b₄ in LSeg |[b₁,b₂]|,|[b₁,b₃]| holds
( b₄ `1 = b₁ & b₂ <= b₄ `2 & b₄ `2 <= b₃ )

proof end;

theorem Th10: :: JGRAPH_6:10

for b₁, b₂, b₃ being real number
for b₄ being Point of (TOP-REAL 2) st b₂ < b₃ & b₄ `1 = b₁ & b₂ <= b₄ `2 & b₄ `2 <= b₃ holds
b₄ in LSeg |[b₁,b₂]|,|[b₁,b₃]|

proof end;

theorem Th11: :: JGRAPH_6:11

for b₁, b₂, b₃ being real number
for b₄ being Point of (TOP-REAL 2) st b₁ <= b₂ & b₄ in LSeg |[b₁,b₃]|,|[b₂,b₃]| holds
( b₄ `2 = b₃ & b₁ <= b₄ `1 & b₄ `1 <= b₂ )

proof end;

theorem Th12: :: JGRAPH_6:12

for b₁, b₂ being real number
for b₃ being Subset of I[01] st b₃ = [.b₁,b₂.] holds
b₃ is closed

proof end;

theorem Th13: :: JGRAPH_6:13

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₃ holds
( dom b₄ = dom b₅ & dom b₄ = the carrier of b₁ & dom b₄ = [#] b₁ )

proof end;

theorem Th14: :: JGRAPH_6:14

for b₁ being non empty TopSpace
for b₂ being non empty Subset of b₁ ex b₃ being Function of (b₁ | b₂),b₁ st
( ( for b₄ being Point of (b₁ | b₂) holds b₃ . b₄ = b₄ ) & b₃ is continuous )

proof end;

theorem Th15: :: JGRAPH_6:15

for b₁ being non empty TopSpace
for b₂ being Function of b₁,R^1
for b₃ being real number st b₂ is continuous holds
ex b₄ being Function of b₁,R^1 st
( ( for b₅ being Point of b₁
for b₆ being real number st b₂ . b₅ = b₆ holds
b₄ . b₅ = b₆ - b₃ ) & b₄ is continuous )

proof end;

theorem Th16: :: JGRAPH_6:16

proof end;

theorem Th17: :: JGRAPH_6:17

for b₁ being non empty TopSpace
for b₂ being Nat
for b₃ being Point of (TOP-REAL b₂)
for b₄ being Function of b₁,R^1 st b₄ is continuous holds
ex b₅ being Function of b₁,(TOP-REAL b₂) st
( ( for b₆ being Point of b₁ holds b₅ . b₆ = (b₄ . b₆) * b₃ ) & b₅ is continuous )

proof end;

theorem Th18: :: JGRAPH_6:18

Sq_Circ . |[(- 1),0]| = |[(- 1),0]|

proof end;

theorem Th19: :: JGRAPH_6:19

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
Sq_Circ . |[(- 1),0]| = W-min b₁ by Th18, JGRAPH_5:32;

theorem Th20: :: JGRAPH_6:20

for b₁ being non empty TopSpace
for b₂ being Nat
for b₃, b₄ being Function of b₁,(TOP-REAL b₂) st b₃ is continuous & b₄ is continuous holds
ex b₅ being Function of b₁,(TOP-REAL b₂) st
( ( for b₆ being Point of b₁ holds b₅ . b₆ = (b₃ . b₆) + (b₄ . b₆) ) & b₅ is continuous )

proof end;

theorem Th21: :: JGRAPH_6:21

for b₁ being non empty TopSpace
for b₂ being Nat
for b₃, b₄ being Point of (TOP-REAL b₂)
for b₅, b₆ being Function of b₁,R^1 st b₅ is continuous & b₆ is continuous holds
ex b₇ being Function of b₁,(TOP-REAL b₂) st
( ( for b₈ being Point of b₁ holds b₇ . b₈ = ((b₅ . b₈) * b₃) + ((b₆ . b₈) * b₄) ) & b₇ is continuous )

proof end;

theorem Th22: :: JGRAPH_6:22

for b₁ being Function
for b₂ being set st b₁ is one-to-one & b₂ c= dom b₁ holds
(b₁ " ) .: (b₁ .: b₂) = b₂

proof end;

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

E26: now

thus |.|[(- 1),0]|.| = sqrt (((- 1) ^2 ) + (0 ^2 )) by Lemma25, JGRAPH_3:10
.= 1 by SQUARE_1:59, SQUARE_1:60, SQUARE_1:61, SQUARE_1:83 ;
thus |.|[1,0]|.| = sqrt ((1 ^2 ) + (0 ^2 )) by Lemma25, JGRAPH_3:10
.= 1 by SQUARE_1:59, SQUARE_1:60, SQUARE_1:83 ;
thus |.|[0,(- 1)]|.| = sqrt ((0 ^2 ) + ((- 1) ^2 )) by Lemma25, 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 Lemma25, JGRAPH_3:10
.= 1 by SQUARE_1:59, SQUARE_1:60, SQUARE_1:83 ;

end;

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

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

theorem Th23: :: JGRAPH_6:23

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

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

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

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

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 } & b₁,b₂,b₃,b₄ are_in_this_order_on 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;

notation

let c₁, c₂, c₃, c₄ be real number ;
synonym rectangle c₁,c₂,c₃,c₄ for [.c₁,c₂,c₃,c₄.];

end;

Lemma34: for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
rectangle b₁,b₂,b₃,b₄ = { b₅ where B is Point of (TOP-REAL 2) : ( ( b₅ `1 = b₁ & b₃ <= b₅ `2 & b₅ `2 <= b₄ ) or ( b₅ `2 = b₄ & b₁ <= b₅ `1 & b₅ `1 <= b₂ ) or ( b₅ `1 = b₂ & b₃ <= b₅ `2 & b₅ `2 <= b₄ ) or ( b₅ `2 = b₃ & b₁ <= b₅ `1 & b₅ `1 <= b₂ ) ) }

proof end;

theorem Th28: :: JGRAPH_6:28

for b₁, b₂, b₃, b₄ being real number
for b₅ being Point of (TOP-REAL 2) st b₁ <= b₂ & b₃ <= b₄ & b₅ in rectangle b₁,b₂,b₃,b₄ holds
( b₁ <= b₅ `1 & b₅ `1 <= b₂ & b₃ <= b₅ `2 & b₅ `2 <= b₄ )

proof end;

definition

let c₁, c₂, c₃, c₄ be real number ;
func inside_of_rectangle c₁,c₂,c₃,c₄ -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 1
{ b₁ where B is Point of (TOP-REAL 2) : ( a₁ < b₁ `1 & b₁ `1 < a₂ & a₃ < b₁ `2 & b₁ `2 < a₄ ) } ;
coherence

proof end;

end;

:: deftheorem Def1 defines inside_of_rectangle JGRAPH_6:def 1 :

definition

let c₁, c₂, c₃, c₄ be real number ;
func closed_inside_of_rectangle c₁,c₂,c₃,c₄ -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 2
{ b₁ where B is Point of (TOP-REAL 2) : ( a₁ <= b₁ `1 & b₁ `1 <= a₂ & a₃ <= b₁ `2 & b₁ `2 <= a₄ ) } ;
coherence

proof end;

end;

:: deftheorem Def2 defines closed_inside_of_rectangle JGRAPH_6:def 2 :

definition

let c₁, c₂, c₃, c₄ be real number ;
func outside_of_rectangle c₁,c₂,c₃,c₄ -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 3
{ b₁ where B is Point of (TOP-REAL 2) : ( not a₁ <= b₁ `1 or not b₁ `1 <= a₂ or not a₃ <= b₁ `2 or not b₁ `2 <= a₄ ) } ;
coherence

proof end;

end;

:: deftheorem Def3 defines outside_of_rectangle JGRAPH_6:def 3 :

definition

let c₁, c₂, c₃, c₄ be real number ;
func closed_outside_of_rectangle c₁,c₂,c₃,c₄ -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 4
{ b₁ where B is Point of (TOP-REAL 2) : ( not a₁ < b₁ `1 or not b₁ `1 < a₂ or not a₃ < b₁ `2 or not b₁ `2 < a₄ ) } ;
coherence

proof end;

end;

:: deftheorem Def4 defines closed_outside_of_rectangle JGRAPH_6:def 4 :

theorem Th29: :: JGRAPH_6:29

for b₁, b₂, b₃ being real number
for b₄, b₅ being Subset of (TOP-REAL 2) st b₃ >= 0 & b₄ = { b₆ where B is Point of (TOP-REAL 2) : |.b₆.| = 1 } & b₅ = { b₆ where B is Point of (TOP-REAL 2) : |.(b₆ - |[b₁,b₂]|).| = b₃ } holds
(AffineMap b₃,b₁,b₃,b₂) .: b₄ = b₅

proof end;

theorem Th30: :: JGRAPH_6:30

for b₁, b₂ being Subset of (TOP-REAL 2) st ex b₃ being Function of ((TOP-REAL 2) | b₁),((TOP-REAL 2) | b₂) st b₃ is_homeomorphism & b₁ is_simple_closed_curve holds
b₂ is_simple_closed_curve

proof end;

theorem Th31: :: JGRAPH_6:31

for b₁ being Subset of (TOP-REAL 2) st b₁ is being_simple_closed_curve holds
b₁ is compact

proof end;

theorem Th32: :: JGRAPH_6:32

for b₁, b₂, b₃ being real number
for b₄ being Subset of (TOP-REAL 2) st b₃ > 0 & b₄ = { b₅ where B is Point of (TOP-REAL 2) : |.(b₅ - |[b₁,b₂]|).| = b₃ } holds
b₄ is_simple_closed_curve

proof end;

definition

let c₁, c₂, c₃ be real number ;
func circle c₁,c₂,c₃ -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 5
{ b₁ where B is Point of (TOP-REAL 2) : |.(b₁ - |[a₁,a₂]|).| = a₃ } ;
coherence

proof end;

end;

:: deftheorem Def5 defines circle JGRAPH_6:def 5 :

registration

let c₁, c₂, c₃ be real number ;
cluster circle a₁,a₂,a₃ -> compact ;
coherence

proof end;

end;

registration

let c₁, c₂ be real number ;
let c₃ be real non negative number ;
cluster circle a₁,a₂,a₃ -> non empty compact ;
coherence

proof end;

end;

definition

let c₁, c₂, c₃ be real number ;
func inside_of_circle c₁,c₂,c₃ -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 6
{ b₁ where B is Point of (TOP-REAL 2) : |.(b₁ - |[a₁,a₂]|).| < a₃ } ;
coherence

proof end;

end;

:: deftheorem Def6 defines inside_of_circle JGRAPH_6:def 6 :

definition

let c₁, c₂, c₃ be real number ;
func closed_inside_of_circle c₁,c₂,c₃ -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 7
{ b₁ where B is Point of (TOP-REAL 2) : |.(b₁ - |[a₁,a₂]|).| <= a₃ } ;
coherence

proof end;

end;

:: deftheorem Def7 defines closed_inside_of_circle JGRAPH_6:def 7 :

definition

let c₁, c₂, c₃ be real number ;
func outside_of_circle c₁,c₂,c₃ -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 8
{ b₁ where B is Point of (TOP-REAL 2) : |.(b₁ - |[a₁,a₂]|).| > a₃ } ;
coherence

proof end;

end;

:: deftheorem Def8 defines outside_of_circle JGRAPH_6:def 8 :

definition

let c₁, c₂, c₃ be real number ;
func closed_outside_of_circle c₁,c₂,c₃ -> Subset of (TOP-REAL 2) equals :: JGRAPH_6:def 9
{ b₁ where B is Point of (TOP-REAL 2) : |.(b₁ - |[a₁,a₂]|).| >= a₃ } ;
coherence

proof end;

end;

:: deftheorem Def9 defines closed_outside_of_circle JGRAPH_6:def 9 :

theorem Th33: :: JGRAPH_6:33

for b₁ being real number holds
( inside_of_circle 0,0,b₁ = { b₂ where B is Point of (TOP-REAL 2) : |.b₂.| < b₁ } & ( b₁ > 0 implies circle 0,0,b₁ = { b₂ where B is Point of (TOP-REAL 2) : |.b₂.| = b₁ } ) & outside_of_circle 0,0,b₁ = { b₂ where B is Point of (TOP-REAL 2) : |.b₂.| > b₁ } & closed_inside_of_circle 0,0,b₁ = { b₂ where B is Point of (TOP-REAL 2) : |.b₂.| <= b₁ } & closed_outside_of_circle 0,0,b₁ = { b₂ where B is Point of (TOP-REAL 2) : |.b₂.| >= b₁ } )

proof end;

theorem Th34: :: JGRAPH_6:34

for b₁, b₂ being Subset of (TOP-REAL 2) st b₁ = { b₃ where B is Point of (TOP-REAL 2) : ( - 1 < b₃ `1 & b₃ `1 < 1 & - 1 < b₃ `2 & b₃ `2 < 1 ) } & b₂ = { b₃ where B is Point of (TOP-REAL 2) : |.b₃.| < 1 } holds
Sq_Circ .: b₁ = b₂

proof end;

theorem Th35: :: JGRAPH_6:35

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

proof end;

theorem Th36: :: JGRAPH_6:36

for b₁, b₂ being Subset of (TOP-REAL 2) st b₁ = { b₃ where B is Point of (TOP-REAL 2) : ( - 1 <= b₃ `1 & b₃ `1 <= 1 & - 1 <= b₃ `2 & b₃ `2 <= 1 ) } & b₂ = { b₃ where B is Point of (TOP-REAL 2) : |.b₃.| <= 1 } holds
Sq_Circ .: b₁ = b₂

proof end;

theorem Th37: :: JGRAPH_6:37

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

proof end;

theorem Th38: :: JGRAPH_6:38

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈ being Subset of (TOP-REAL 2)
for b₉ being non empty compact Subset of (TOP-REAL 2)
for b₁₀ being Function of (TOP-REAL 2),(TOP-REAL 2) st b₉ = circle 0,0,1 & b₁ = inside_of_circle 0,0,1 & b₂ = outside_of_circle 0,0,1 & b₃ = closed_inside_of_circle 0,0,1 & b₄ = closed_outside_of_circle 0,0,1 & b₅ = inside_of_rectangle (- 1),1,(- 1),1 & b₆ = outside_of_rectangle (- 1),1,(- 1),1 & b₇ = closed_inside_of_rectangle (- 1),1,(- 1),1 & b₈ = closed_outside_of_rectangle (- 1),1,(- 1),1 & b₁₀ = Sq_Circ holds
( b₁₀ .: (rectangle (- 1),1,(- 1),1) = b₉ & (b₁₀ " ) .: b₉ = rectangle (- 1),1,(- 1),1 & b₁₀ .: b₅ = b₁ & (b₁₀ " ) .: b₁ = b₅ & b₁₀ .: b₆ = b₂ & (b₁₀ " ) .: b₂ = b₆ & b₁₀ .: b₇ = b₃ & b₁₀ .: b₈ = b₄ & (b₁₀ " ) .: b₃ = b₇ & (b₁₀ " ) .: b₄ = b₈ )

proof end;

theorem Th39: :: JGRAPH_6:39

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
( LSeg |[b₁,b₃]|,|[b₁,b₄]| = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 = b₁ & b₅ `2 <= b₄ & b₅ `2 >= b₃ ) } & LSeg |[b₁,b₄]|,|[b₂,b₄]| = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 <= b₂ & b₅ `1 >= b₁ & b₅ `2 = b₄ ) } & LSeg |[b₁,b₃]|,|[b₂,b₃]| = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 <= b₂ & b₅ `1 >= b₁ & b₅ `2 = b₃ ) } & LSeg |[b₂,b₃]|,|[b₂,b₄]| = { b₅ where B is Point of (TOP-REAL 2) : ( b₅ `1 = b₂ & b₅ `2 <= b₄ & b₅ `2 >= b₃ ) } )

proof end;

theorem Th40: :: JGRAPH_6:40

canceled;

theorem Th41: :: JGRAPH_6:41

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
(LSeg |[b₁,b₃]|,|[b₁,b₄]|) /\ (LSeg |[b₁,b₃]|,|[b₂,b₃]|) = {|[b₁,b₃]|}

proof end;

theorem Th42: :: JGRAPH_6:42

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
(LSeg |[b₁,b₃]|,|[b₂,b₃]|) /\ (LSeg |[b₂,b₃]|,|[b₂,b₄]|) = {|[b₂,b₃]|}

proof end;

theorem Th43: :: JGRAPH_6:43

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
(LSeg |[b₁,b₄]|,|[b₂,b₄]|) /\ (LSeg |[b₂,b₃]|,|[b₂,b₄]|) = {|[b₂,b₄]|}

proof end;

theorem Th44: :: JGRAPH_6:44

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
(LSeg |[b₁,b₃]|,|[b₁,b₄]|) /\ (LSeg |[b₁,b₄]|,|[b₂,b₄]|) = {|[b₁,b₄]|}

proof end;

theorem Th45: :: JGRAPH_6:45

{ b₁ where B is Point of (TOP-REAL 2) : ( ( - 1 = b₁ `1 & - 1 <= b₁ `2 & b₁ `2 <= 1 ) or ( b₁ `1 = 1 & - 1 <= b₁ `2 & b₁ `2 <= 1 ) or ( - 1 = b₁ `2 & - 1 <= b₁ `1 & b₁ `1 <= 1 ) or ( 1 = b₁ `2 & - 1 <= b₁ `1 & b₁ `1 <= 1 ) ) } = { b₁ where B is Point of (TOP-REAL 2) : ( ( b₁ `1 = - 1 & - 1 <= b₁ `2 & b₁ `2 <= 1 ) or ( b₁ `2 = 1 & - 1 <= b₁ `1 & b₁ `1 <= 1 ) or ( b₁ `1 = 1 & - 1 <= b₁ `2 & b₁ `2 <= 1 ) or ( b₁ `2 = - 1 & - 1 <= b₁ `1 & b₁ `1 <= 1 ) ) }

proof end;

theorem Th46: :: JGRAPH_6:46

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
W-bound (rectangle b₁,b₂,b₃,b₄) = b₁

proof end;

theorem Th47: :: JGRAPH_6:47

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
N-bound (rectangle b₁,b₂,b₃,b₄) = b₄

proof end;

theorem Th48: :: JGRAPH_6:48

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
E-bound (rectangle b₁,b₂,b₃,b₄) = b₂

proof end;

theorem Th49: :: JGRAPH_6:49

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
S-bound (rectangle b₁,b₂,b₃,b₄) = b₃

proof end;

theorem Th50: :: JGRAPH_6:50

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
NW-corner (rectangle b₁,b₂,b₃,b₄) = |[b₁,b₄]|

proof end;

theorem Th51: :: JGRAPH_6:51

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
NE-corner (rectangle b₁,b₂,b₃,b₄) = |[b₂,b₄]|

proof end;

theorem Th52: :: JGRAPH_6:52

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
SW-corner (rectangle b₁,b₂,b₃,b₄) = |[b₁,b₃]|

proof end;

theorem Th53: :: JGRAPH_6:53

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
SE-corner (rectangle b₁,b₂,b₃,b₄) = |[b₂,b₃]|

proof end;

theorem Th54: :: JGRAPH_6:54

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
W-most (rectangle b₁,b₂,b₃,b₄) = LSeg |[b₁,b₃]|,|[b₁,b₄]|

proof end;

theorem Th55: :: JGRAPH_6:55

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
E-most (rectangle b₁,b₂,b₃,b₄) = LSeg |[b₂,b₃]|,|[b₂,b₄]|

proof end;

theorem Th56: :: JGRAPH_6:56

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
( W-min (rectangle b₁,b₂,b₃,b₄) = |[b₁,b₃]| & E-max (rectangle b₁,b₂,b₃,b₄) = |[b₂,b₄]| )

proof end;

theorem Th57: :: JGRAPH_6:57

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & b₃ < b₄ holds
( (LSeg |[b₁,b₃]|,|[b₁,b₄]|) \/ (LSeg |[b₁,b₄]|,|[b₂,b₄]|) is_an_arc_of W-min (rectangle b₁,b₂,b₃,b₄), E-max (rectangle b₁,b₂,b₃,b₄) & (LSeg |[b₁,b₃]|,|[b₂,b₃]|) \/ (LSeg |[b₂,b₃]|,|[b₂,b₄]|) is_an_arc_of E-max (rectangle b₁,b₂,b₃,b₄), W-min (rectangle b₁,b₂,b₃,b₄) )

proof end;

theorem Th58: :: JGRAPH_6:58

for b₁, b₂, b₃, b₄ being real number
for b₅, b₆ being FinSequence of (TOP-REAL 2)
for b₇, b₈, b₉, b₁₀ being Point of (TOP-REAL 2) st b₁ < b₂ & b₃ < b₄ & b₇ = |[b₁,b₃]| & b₈ = |[b₂,b₄]| & b₉ = |[b₁,b₄]| & b₁₀ = |[b₂,b₃]| & b₅ = <*b₇,b₉,b₈*> & b₆ = <*b₇,b₁₀,b₈*> holds
( b₅ is_S-Seq & L~ b₅ = (LSeg b₇,b₉) \/ (LSeg b₉,b₈) & b₆ is_S-Seq & L~ b₆ = (LSeg b₇,b₁₀) \/ (LSeg b₁₀,b₈) & rectangle b₁,b₂,b₃,b₄ = (L~ b₅) \/ (L~ b₆) & (L~ b₅) /\ (L~ b₆) = {b₇,b₈} & b₅ /. 1 = b₇ & b₅ /. (len b₅) = b₈ & b₆ /. 1 = b₇ & b₆ /. (len b₆) = b₈ )

proof end;

theorem Th59: :: JGRAPH_6:59

for b₁, b₂ being Subset of (TOP-REAL 2)
for b₃, b₄, b₅, b₆ being real number
for b₇, b₈ being FinSequence of (TOP-REAL 2)
for b₉, b₁₀ being Point of (TOP-REAL 2) st b₃ < b₄ & b₅ < b₆ & b₉ = |[b₃,b₅]| & b₁₀ = |[b₄,b₆]| & b₇ = <*|[b₃,b₅]|,|[b₃,b₆]|,|[b₄,b₆]|*> & b₈ = <*|[b₃,b₅]|,|[b₄,b₅]|,|[b₄,b₆]|*> & b₁ = L~ b₇ & b₂ = L~ b₈ holds
( b₁ is_an_arc_of b₉,b₁₀ & b₂ is_an_arc_of b₉,b₁₀ & not b₁ is empty & not b₂ is empty & rectangle b₃,b₄,b₅,b₆ = b₁ \/ b₂ & b₁ /\ b₂ = {b₉,b₁₀} )

proof end;

theorem Th60: :: JGRAPH_6:60

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & b₃ < b₄ holds
rectangle b₁,b₂,b₃,b₄ is_simple_closed_curve

proof end;

theorem Th61: :: JGRAPH_6:61

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & b₃ < b₄ holds
Upper_Arc (rectangle b₁,b₂,b₃,b₄) = (LSeg |[b₁,b₃]|,|[b₁,b₄]|) \/ (LSeg |[b₁,b₄]|,|[b₂,b₄]|)

proof end;

theorem Th62: :: JGRAPH_6:62

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & b₃ < b₄ holds
Lower_Arc (rectangle b₁,b₂,b₃,b₄) = (LSeg |[b₁,b₃]|,|[b₂,b₃]|) \/ (LSeg |[b₂,b₃]|,|[b₂,b₄]|)

proof end;

theorem Th63: :: JGRAPH_6:63

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & b₃ < b₄ holds
ex b₅ being Function of I[01] ,((TOP-REAL 2) | (Upper_Arc (rectangle b₁,b₂,b₃,b₄))) st
( b₅ is_homeomorphism & b₅ . 0 = W-min (rectangle b₁,b₂,b₃,b₄) & b₅ . 1 = E-max (rectangle b₁,b₂,b₃,b₄) & rng b₅ = Upper_Arc (rectangle b₁,b₂,b₃,b₄) & ( for b₆ being Real st b₆ in [.0,(1 / 2).] holds
b₅ . b₆ = ((1 - (2 * b₆)) * |[b₁,b₃]|) + ((2 * b₆) * |[b₁,b₄]|) ) & ( for b₆ being Real st b₆ in [.(1 / 2),1.] holds
b₅ . b₆ = ((1 - ((2 * b₆) - 1)) * |[b₁,b₄]|) + (((2 * b₆) - 1) * |[b₂,b₄]|) ) & ( for b₆ being Point of (TOP-REAL 2) st b₆ in LSeg |[b₁,b₃]|,|[b₁,b₄]| holds
( 0 <= (((b₆ `2 ) - b₃) / (b₄ - b₃)) / 2 & (((b₆ `2 ) - b₃) / (b₄ - b₃)) / 2 <= 1 & b₅ . ((((b₆ `2 ) - b₃) / (b₄ - b₃)) / 2) = b₆ ) ) & ( for b₆ being Point of (TOP-REAL 2) st b₆ in LSeg |[b₁,b₄]|,|[b₂,b₄]| holds
( 0 <= ((((b₆ `1 ) - b₁) / (b₂ - b₁)) / 2) + (1 / 2) & ((((b₆ `1 ) - b₁) / (b₂ - b₁)) / 2) + (1 / 2) <= 1 & b₅ . (((((b₆ `1 ) - b₁) / (b₂ - b₁)) / 2) + (1 / 2)) = b₆ ) ) )

proof end;

theorem Th64: :: JGRAPH_6:64

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & b₃ < b₄ holds
ex b₅ being Function of I[01] ,((TOP-REAL 2) | (Lower_Arc (rectangle b₁,b₂,b₃,b₄))) st
( b₅ is_homeomorphism & b₅ . 0 = E-max (rectangle b₁,b₂,b₃,b₄) & b₅ . 1 = W-min (rectangle b₁,b₂,b₃,b₄) & rng b₅ = Lower_Arc (rectangle b₁,b₂,b₃,b₄) & ( for b₆ being Real st b₆ in [.0,(1 / 2).] holds
b₅ . b₆ = ((1 - (2 * b₆)) * |[b₂,b₄]|) + ((2 * b₆) * |[b₂,b₃]|) ) & ( for b₆ being Real st b₆ in [.(1 / 2),1.] holds
b₅ . b₆ = ((1 - ((2 * b₆) - 1)) * |[b₂,b₃]|) + (((2 * b₆) - 1) * |[b₁,b₃]|) ) & ( for b₆ being Point of (TOP-REAL 2) st b₆ in LSeg |[b₂,b₄]|,|[b₂,b₃]| holds
( 0 <= (((b₆ `2 ) - b₄) / (b₃ - b₄)) / 2 & (((b₆ `2 ) - b₄) / (b₃ - b₄)) / 2 <= 1 & b₅ . ((((b₆ `2 ) - b₄) / (b₃ - b₄)) / 2) = b₆ ) ) & ( for b₆ being Point of (TOP-REAL 2) st b₆ in LSeg |[b₂,b₃]|,|[b₁,b₃]| holds
( 0 <= ((((b₆ `1 ) - b₂) / (b₁ - b₂)) / 2) + (1 / 2) & ((((b₆ `1 ) - b₂) / (b₁ - b₂)) / 2) + (1 / 2) <= 1 & b₅ . (((((b₆ `1 ) - b₂) / (b₁ - b₂)) / 2) + (1 / 2)) = b₆ ) ) )

proof end;

theorem Th65: :: JGRAPH_6:65

for b₁, b₂, b₃, b₄ being real number
for b₅, b₆ being Point of (TOP-REAL 2) st b₁ < b₂ & b₃ < b₄ & b₅ in LSeg |[b₁,b₃]|,|[b₁,b₄]| & b₆ in LSeg |[b₁,b₃]|,|[b₁,b₄]| holds
( LE b₅,b₆, rectangle b₁,b₂,b₃,b₄ iff b₅ `2 <= b₆ `2 )

proof end;

theorem Th66: :: JGRAPH_6:66

for b₁, b₂, b₃, b₄ being real number
for b₅, b₆ being Point of (TOP-REAL 2) st b₁ < b₂ & b₃ < b₄ & b₅ in LSeg |[b₁,b₄]|,|[b₂,b₄]| & b₆ in LSeg |[b₁,b₄]|,|[b₂,b₄]| holds
( LE b₅,b₆, rectangle b₁,b₂,b₃,b₄ iff b₅ `1 <= b₆ `1 )

proof end;

theorem Th67: :: JGRAPH_6:67

for b₁, b₂, b₃, b₄ being real number
for b₅, b₆ being Point of (TOP-REAL 2) st b₁ < b₂ & b₃ < b₄ & b₅ in LSeg |[b₂,b₃]|,|[b₂,b₄]| & b₆ in LSeg |[b₂,b₃]|,|[b₂,b₄]| holds
( LE b₅,b₆, rectangle b₁,b₂,b₃,b₄ iff b₅ `2 >= b₆ `2 )

proof end;

theorem Th68: :: JGRAPH_6:68

for b₁, b₂, b₃, b₄ being real number
for b₅, b₆ being Point of (TOP-REAL 2) st b₁ < b₂ & b₃ < b₄ & b₅ in LSeg |[b₁,b₃]|,|[b₂,b₃]| & b₆ in LSeg |[b₁,b₃]|,|[b₂,b₃]| holds
( LE b₅,b₆, rectangle b₁,b₂,b₃,b₄ & b₅ <> W-min (rectangle b₁,b₂,b₃,b₄) iff ( b₅ `1 >= b₆ `1 & b₆ <> W-min (rectangle b₁,b₂,b₃,b₄) ) )

proof end;

theorem Th69: :: JGRAPH_6:69

for b₁, b₂, b₃, b₄ being real number
for b₅, b₆ being Point of (TOP-REAL 2) st b₁ < b₂ & b₃ < b₄ & b₅ in LSeg |[b₁,b₃]|,|[b₁,b₄]| holds
( LE b₅,b₆, rectangle b₁,b₂,b₃,b₄ iff ( ( b₆ in LSeg |[b₁,b₃]|,|[b₁,b₄]| & b₅ `2 <= b₆ `2 ) or b₆ in LSeg |[b₁,b₄]|,|[b₂,b₄]| or b₆ in LSeg |[b₂,b₄]|,|[b₂,b₃]| or ( b₆ in LSeg |[b₂,b₃]|,|[b₁,b₃]| & b₆ <> W-min (rectangle b₁,b₂,b₃,b₄) ) ) )

proof end;

theorem Th70: :: JGRAPH_6:70

for b₁, b₂, b₃, b₄ being real number
for b₅, b₆ being Point of (TOP-REAL 2) st b₁ < b₂ & b₃ < b₄ & b₅ in LSeg |[b₁,b₄]|,|[b₂,b₄]| holds
( LE b₅,b₆, rectangle b₁,b₂,b₃,b₄ iff ( ( b₆ in LSeg |[b₁,b₄]|,|[b₂,b₄]| & b₅ `1 <= b₆ `1 ) or b₆ in LSeg |[b₂,b₄]|,|[b₂,b₃]| or ( b₆ in LSeg |[b₂,b₃]|,|[b₁,b₃]| & b₆ <> W-min (rectangle b₁,b₂,b₃,b₄) ) ) )

proof end;

theorem Th71: :: JGRAPH_6:71

for b₁, b₂, b₃, b₄ being real number
for b₅, b₆ being Point of (TOP-REAL 2) st b₁ < b₂ & b₃ < b₄ & b₅ in LSeg |[b₂,b₄]|,|[b₂,b₃]| holds
( LE b₅,b₆, rectangle b₁,b₂,b₃,b₄ iff ( ( b₆ in LSeg |[b₂,b₄]|,|[b₂,b₃]| & b₅ `2 >= b₆ `2 ) or ( b₆ in LSeg |[b₂,b₃]|,|[b₁,b₃]| & b₆ <> W-min (rectangle b₁,b₂,b₃,b₄) ) ) )

proof end;

theorem Th72: :: JGRAPH_6:72

for b₁, b₂, b₃, b₄ being real number
for b₅, b₆ being Point of (TOP-REAL 2) st b₁ < b₂ & b₃ < b₄ & b₅ in LSeg |[b₂,b₃]|,|[b₁,b₃]| & b₅ <> W-min (rectangle b₁,b₂,b₃,b₄) holds
( LE b₅,b₆, rectangle b₁,b₂,b₃,b₄ iff ( b₆ in LSeg |[b₂,b₃]|,|[b₁,b₃]| & b₅ `1 >= b₆ `1 & b₆ <> W-min (rectangle b₁,b₂,b₃,b₄) ) )

proof end;

theorem Th73: :: JGRAPH_6:73

for b₁ being set
for b₂, b₃, b₄, b₅ being real number st b₁ in rectangle b₂,b₃,b₄,b₅ & b₂ < b₃ & b₄ < b₅ & not b₁ in LSeg |[b₂,b₄]|,|[b₂,b₅]| & not b₁ in LSeg |[b₂,b₅]|,|[b₃,b₅]| & not b₁ in LSeg |[b₃,b₅]|,|[b₃,b₄]| holds
b₁ in LSeg |[b₃,b₄]|,|[b₂,b₄]|

proof end;

theorem Th74: :: JGRAPH_6:74

for b₁, b₂ being Point of (TOP-REAL 2) st LE b₁,b₂, rectangle (- 1),1,(- 1),1 & b₁ in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & not ( b₂ in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & b₂ `2 >= b₁ `2 ) & not b₂ in LSeg |[(- 1),1]|,|[1,1]| & not b₂ in LSeg |[1,1]|,|[1,(- 1)]| holds
( b₂ in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| & b₂ <> |[(- 1),(- 1)]| )

proof end;

theorem Th75: :: JGRAPH_6:75

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2)
for b₄ being Function of (TOP-REAL 2),(TOP-REAL 2) st b₃ = circle 0,0,1 & b₄ = Sq_Circ & b₁ in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & b₁ `2 >= 0 & LE b₁,b₂, rectangle (- 1),1,(- 1),1 holds
LE b₄ . b₁,b₄ . b₂,b₃

proof end;

theorem Th76: :: JGRAPH_6:76

for b₁, b₂, b₃ being Point of (TOP-REAL 2)
for b₄ being non empty compact Subset of (TOP-REAL 2)
for b₅ being Function of (TOP-REAL 2),(TOP-REAL 2) st b₄ = circle 0,0,1 & b₅ = Sq_Circ & b₁ in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & b₁ `2 >= 0 & LE b₁,b₂, rectangle (- 1),1,(- 1),1 & LE b₂,b₃, rectangle (- 1),1,(- 1),1 holds
LE b₅ . b₂,b₅ . b₃,b₄

proof end;

theorem Th77: :: JGRAPH_6:77

for b₁ being Point of (TOP-REAL 2)
for b₂ being Function of (TOP-REAL 2),(TOP-REAL 2) st b₂ = Sq_Circ & b₁ `1 = - 1 & b₁ `2 < 0 holds
( (b₂ . b₁) `1 < 0 & (b₂ . b₁) `2 < 0 )

proof end;

theorem Th78: :: JGRAPH_6:78

for b₁ being Point of (TOP-REAL 2)
for b₂ being non empty compact Subset of (TOP-REAL 2)
for b₃ being Function of (TOP-REAL 2),(TOP-REAL 2) st b₂ = circle 0,0,1 & b₃ = Sq_Circ holds
( (b₃ . b₁) `1 >= 0 iff b₁ `1 >= 0 )

proof end;

theorem Th79: :: JGRAPH_6:79

proof end;

theorem Th80: :: JGRAPH_6:80

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being Function of (TOP-REAL 2),(TOP-REAL 2) st b₃ = Sq_Circ & b₁ in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & b₂ in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| holds
(b₃ . b₁) `1 <= (b₃ . b₂) `1

proof end;

theorem Th81: :: JGRAPH_6:81

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being Function of (TOP-REAL 2),(TOP-REAL 2) st b₃ = Sq_Circ & b₁ in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & b₂ in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & b₁ `2 >= b₂ `2 & b₁ `2 < 0 holds
(b₃ . b₁) `2 >= (b₃ . b₂) `2

proof end;

theorem Th82: :: JGRAPH_6:82

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 Function of (TOP-REAL 2),(TOP-REAL 2) st b₅ = circle 0,0,1 & b₆ = Sq_Circ & LE b₁,b₂, rectangle (- 1),1,(- 1),1 & LE b₂,b₃, rectangle (- 1),1,(- 1),1 & LE b₃,b₄, rectangle (- 1),1,(- 1),1 holds
b₆ . b₁,b₆ . b₂,b₆ . b₃,b₆ . b₄ are_in_this_order_on b₅

proof end;

theorem Th83: :: JGRAPH_6:83

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being non empty compact Subset of (TOP-REAL 2) st b₃ is_simple_closed_curve & b₁ in b₃ & b₂ in b₃ & not LE b₁,b₂,b₃ holds
LE b₂,b₁,b₃

proof end;

theorem Th84: :: JGRAPH_6:84

for b₁, b₂, b₃ being Point of (TOP-REAL 2)
for b₄ being non empty compact Subset of (TOP-REAL 2) st b₄ is_simple_closed_curve & b₁ in b₄ & b₂ in b₄ & b₃ in b₄ & not ( LE b₁,b₂,b₄ & LE b₂,b₃,b₄ ) & not ( LE b₁,b₃,b₄ & LE b₃,b₂,b₄ ) & not ( LE b₂,b₁,b₄ & LE b₁,b₃,b₄ ) & not ( LE b₂,b₃,b₄ & LE b₃,b₁,b₄ ) & not ( LE b₃,b₁,b₄ & LE b₁,b₂,b₄ ) holds
( LE b₃,b₂,b₄ & LE b₂,b₁,b₄ ) by Th83;

theorem Th85: :: JGRAPH_6:85

for b₁, b₂, b₃ being Point of (TOP-REAL 2)
for b₄ being non empty compact Subset of (TOP-REAL 2) st b₄ is_simple_closed_curve & b₁ in b₄ & b₂ in b₄ & b₃ in b₄ & LE b₂,b₃,b₄ & not LE b₁,b₂,b₄ & not ( LE b₂,b₁,b₄ & LE b₁,b₃,b₄ ) holds
LE b₃,b₁,b₄ by Th83;

theorem Th86: :: JGRAPH_6:86

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being non empty compact Subset of (TOP-REAL 2) st b₅ is_simple_closed_curve & b₁ in b₅ & b₂ in b₅ & b₃ in b₅ & b₄ in b₅ & LE b₂,b₃,b₅ & LE b₃,b₄,b₅ & not LE b₁,b₂,b₅ & not ( LE b₂,b₁,b₅ & LE b₁,b₃,b₅ ) & not ( LE b₃,b₁,b₅ & LE b₁,b₄,b₅ ) holds
LE b₄,b₁,b₅ by Th83;

theorem Th87: :: JGRAPH_6:87

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 Function of (TOP-REAL 2),(TOP-REAL 2) st b₅ = circle 0,0,1 & b₆ = Sq_Circ & LE b₆ . b₁,b₆ . b₂,b₅ & LE b₆ . b₂,b₆ . b₃,b₅ & LE b₆ . b₃,b₆ . b₄,b₅ holds
b₁,b₂,b₃,b₄ are_in_this_order_on rectangle (- 1),1,(- 1),1

proof end;

theorem Th88: :: JGRAPH_6:88

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 Function of (TOP-REAL 2),(TOP-REAL 2) st b₅ = circle 0,0,1 & b₆ = Sq_Circ holds
( b₁,b₂,b₃,b₄ are_in_this_order_on rectangle (- 1),1,(- 1),1 iff b₆ . b₁,b₆ . b₂,b₆ . b₃,b₆ . b₄ are_in_this_order_on b₅ )

proof end;

theorem Th89: :: JGRAPH_6:89

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being Subset of (TOP-REAL 2) st b₁,b₂,b₃,b₄ are_in_this_order_on rectangle (- 1),1,(- 1),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₅ = closed_inside_of_rectangle (- 1),1,(- 1),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;