:: JGRAPH_6 semantic presentation

theorem :: JGRAPH_6:1

canceled;

theorem Th2: :: JGRAPH_6:2

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

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

theorem :: JGRAPH_6:3

canceled;

theorem Th4: :: JGRAPH_6:4

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

proof end;

theorem Th5: :: JGRAPH_6:5

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

proof end;

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

proof end;

theorem Th6: :: JGRAPH_6:6

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

proof end;

theorem Th7: :: JGRAPH_6:7

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th8: :: JGRAPH_6:8

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

proof end;

theorem Th9: :: JGRAPH_6:9

for a, c, d being real number
for p being Point of (TOP-REAL 2) st c <= d & p in LSeg |[a,c]|,|[a,d]| holds
( p `1 = a & c <= p `2 & p `2 <= d )

proof end;

theorem Th10: :: JGRAPH_6:10

for a, c, d being real number
for p being Point of (TOP-REAL 2) st c < d & p `1 = a & c <= p `2 & p `2 <= d holds
p in LSeg |[a,c]|,|[a,d]|

proof end;

theorem Th11: :: JGRAPH_6:11

for a, b, d being real number
for p being Point of (TOP-REAL 2) st a <= b & p in LSeg |[a,d]|,|[b,d]| holds
( p `2 = d & a <= p `1 & p `1 <= b )

proof end;

theorem Th12: :: JGRAPH_6:12

for a, b being real number
for B being Subset of I[01] st B = [.a,b.] holds
B is closed

proof end;

theorem Th13: :: JGRAPH_6:13

for X being TopStruct
for Y, Z being non empty TopStruct
for f being Function of X,Y
for g being Function of X,Z holds
( dom f = dom g & dom f = the carrier of X & dom f = [#] X )

proof end;

theorem Th14: :: JGRAPH_6:14

for X being non empty TopSpace
for B being non empty Subset of X ex f being Function of (X | B),X st
( ( for p being Point of (X | B) holds f . p = p ) & f is continuous )

proof end;

theorem Th15: :: JGRAPH_6:15

for X being non empty TopSpace
for f1 being Function of X,R^1
for a being real number st f1 is continuous holds
ex g being Function of X,R^1 st
( ( for p being Point of X
for r1 being real number st f1 . p = r1 holds
g . p = r1 - a ) & g is continuous )

proof end;

theorem Th16: :: JGRAPH_6:16

proof end;

theorem Th17: :: JGRAPH_6:17

for X being non empty TopSpace
for n being Nat
for p being Point of (TOP-REAL n)
for f being Function of X,R^1 st f is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (f . r) * p ) & g is continuous )

proof end;

theorem Th18: :: JGRAPH_6:18

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

proof end;

theorem :: JGRAPH_6:19

for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } holds
Sq_Circ . |[(- 1),0]| = W-min P by Th18, JGRAPH_5:32;

theorem Th20: :: JGRAPH_6:20

for X being non empty TopSpace
for n being Nat
for g1, g2 being Function of X,(TOP-REAL n) st g1 is continuous & g2 is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = (g1 . r) + (g2 . r) ) & g is continuous )

proof end;

theorem Th21: :: JGRAPH_6:21

for X being non empty TopSpace
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for f1, f2 being Function of X,R^1 st f1 is continuous & f2 is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for r being Point of X holds g . r = ((f1 . r) * p1) + ((f2 . r) * p2) ) & g is continuous )

proof end;

theorem Th22: :: JGRAPH_6:22

for f being Function
for A being set st f is one-to-one & A c= dom f holds
(f " ) .: (f .: A) = A

proof end;

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

Lm7: now

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

end;

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

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

theorem Th23: :: JGRAPH_6:23

for f, g being Function of I[01] ,(TOP-REAL 2)
for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)
for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1 ) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1 ) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1 ) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1 ) ) } & f . O in KXP & f . I in KXN & 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 Th24: :: JGRAPH_6:24

for f, g being Function of I[01] ,(TOP-REAL 2)
for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)
for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| <= 1 } & KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1 ) ) } & KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1 ) ) } & KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1 ) ) } & KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1 ) ) } & f . O in KXP & f . I in KXN & 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 Th25: :: JGRAPH_6:25

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
for f, g being Function of I[01] ,(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

proof end;

theorem Th26: :: JGRAPH_6:26

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
for f, g being Function of I[01] ,(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } & f . 0 = p3 & f . 1 = p1 & g . 0 = p4 & g . 1 = p2 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g

proof end;

theorem Th27: :: JGRAPH_6:27

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & p1,p2,p3,p4 are_in_this_order_on P holds
for f, g being Function of I[01] ,(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 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;

notation

let a, b, c, d be real number ;
synonym rectangle a,b,c,d for [.a,b,c,d.];

end;

Lm10: for a, b, c, d being real number st a <= b & c <= d holds
rectangle a,b,c,d = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = a & c <= p `2 & p `2 <= d ) or ( p `2 = d & a <= p `1 & p `1 <= b ) or ( p `1 = b & c <= p `2 & p `2 <= d ) or ( p `2 = c & a <= p `1 & p `1 <= b ) ) }

proof end;

theorem Th28: :: JGRAPH_6:28

for a, b, c, d being real number
for p being Point of (TOP-REAL 2) st a <= b & c <= d & p in rectangle a,b,c,d holds
( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d )

proof end;

definition

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

proof end;

end;

:: deftheorem defines inside_of_rectangle JGRAPH_6:def 1 :

definition

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

proof end;

end;

:: deftheorem defines closed_inside_of_rectangle JGRAPH_6:def 2 :

definition

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

proof end;

end;

:: deftheorem defines outside_of_rectangle JGRAPH_6:def 3 :

definition

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

proof end;

end;

:: deftheorem defines closed_outside_of_rectangle JGRAPH_6:def 4 :

theorem Th29: :: JGRAPH_6:29

for a, b, r being real number
for Kb, Cb being Subset of (TOP-REAL 2) st r >= 0 & Kb = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.(p2 - |[a,b]|).| = r } holds
(AffineMap r,a,r,b) .: Kb = Cb

proof end;

theorem Th30: :: JGRAPH_6:30

for P, Q being Subset of (TOP-REAL 2) st ex f being Function of ((TOP-REAL 2) | P),((TOP-REAL 2) | Q) st f is_homeomorphism & P is_simple_closed_curve holds
Q is_simple_closed_curve

proof end;

theorem Th31: :: JGRAPH_6:31

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

proof end;

theorem Th32: :: JGRAPH_6:32

for a, b, r being real number
for Cb being Subset of (TOP-REAL 2) st r > 0 & Cb = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } holds
Cb is_simple_closed_curve

proof end;

definition

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

proof end;

end;

:: deftheorem defines circle JGRAPH_6:def 5 :

registration

let a, b, r be real number ;
cluster circle a,b,r -> compact ;
coherence

proof end;

end;

registration

let a, b be real number ;
let r be real non negative number ;
cluster circle a,b,r -> non empty compact ;
coherence

proof end;

end;

definition

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

proof end;

end;

:: deftheorem defines inside_of_circle JGRAPH_6:def 6 :

definition

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

proof end;

end;

:: deftheorem defines closed_inside_of_circle JGRAPH_6:def 7 :

definition

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

proof end;

end;

:: deftheorem defines outside_of_circle JGRAPH_6:def 8 :

definition

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

proof end;

end;

:: deftheorem defines closed_outside_of_circle JGRAPH_6:def 9 :

theorem Th33: :: JGRAPH_6:33

for r being real number holds
( inside_of_circle 0,0,r = { p where p is Point of (TOP-REAL 2) : |.p.| < r } & ( r > 0 implies circle 0,0,r = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| = r } ) & outside_of_circle 0,0,r = { p3 where p3 is Point of (TOP-REAL 2) : |.p3.| > r } & closed_inside_of_circle 0,0,r = { q where q is Point of (TOP-REAL 2) : |.q.| <= r } & closed_outside_of_circle 0,0,r = { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r } )

proof end;

theorem Th34: :: JGRAPH_6:34

for Kb, Cb being Subset of (TOP-REAL 2) st Kb = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| < 1 } holds
Sq_Circ .: Kb = Cb

proof end;

theorem Th35: :: JGRAPH_6:35

for Kb, Cb being Subset of (TOP-REAL 2) st Kb = { p where p is Point of (TOP-REAL 2) : ( not - 1 <= p `1 or not p `1 <= 1 or not - 1 <= p `2 or not p `2 <= 1 ) } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| > 1 } holds
Sq_Circ .: Kb = Cb

proof end;

theorem Th36: :: JGRAPH_6:36

for Kb, Cb being Subset of (TOP-REAL 2) st Kb = { p where p is Point of (TOP-REAL 2) : ( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 ) } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| <= 1 } holds
Sq_Circ .: Kb = Cb

proof end;

theorem Th37: :: JGRAPH_6:37

for Kb, Cb being Subset of (TOP-REAL 2) st Kb = { p where p is Point of (TOP-REAL 2) : ( not - 1 = 1 } holds
Sq_Circ .: Kb = Cb

proof end;

theorem :: JGRAPH_6:38

for P0, P1, P01, P11, K0, K1, K01, K11 being Subset of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle 0,0,1 & P0 = inside_of_circle 0,0,1 & P1 = outside_of_circle 0,0,1 & P01 = closed_inside_of_circle 0,0,1 & P11 = closed_outside_of_circle 0,0,1 & K0 = inside_of_rectangle (- 1),1,(- 1),1 & K1 = outside_of_rectangle (- 1),1,(- 1),1 & K01 = closed_inside_of_rectangle (- 1),1,(- 1),1 & K11 = closed_outside_of_rectangle (- 1),1,(- 1),1 & f = Sq_Circ holds
( f .: (rectangle (- 1),1,(- 1),1) = P & (f " ) .: P = rectangle (- 1),1,(- 1),1 & f .: K0 = P0 & (f " ) .: P0 = K0 & f .: K1 = P1 & (f " ) .: P1 = K1 & f .: K01 = P01 & f .: K11 = P11 & (f " ) .: P01 = K01 & (f " ) .: P11 = K11 )

proof end;

theorem Th39: :: JGRAPH_6:39

for a, b, c, d being real number st a <= b & c <= d holds
( LSeg |[a,c]|,|[a,d]| = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = a & p1 `2 <= d & p1 `2 >= c ) } & LSeg |[a,d]|,|[b,d]| = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } & LSeg |[a,c]|,|[b,c]| = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } & LSeg |[b,c]|,|[b,d]| = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } )

proof end;

theorem :: JGRAPH_6:40

canceled;

theorem Th41: :: JGRAPH_6:41

for a, b, c, d being real number st a <= b & c <= d holds
(LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,c]|,|[b,c]|) = {|[a,c]|}

proof end;

theorem Th42: :: JGRAPH_6:42

for a, b, c, d being real number st a <= b & c <= d holds
(LSeg |[a,c]|,|[b,c]|) /\ (LSeg |[b,c]|,|[b,d]|) = {|[b,c]|}

proof end;

theorem Th43: :: JGRAPH_6:43

for a, b, c, d being real number st a <= b & c <= d holds
(LSeg |[a,d]|,|[b,d]|) /\ (LSeg |[b,c]|,|[b,d]|) = {|[b,d]|}

proof end;

theorem Th44: :: JGRAPH_6:44

for a, b, c, d being real number st a <= b & c <= d holds
(LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) = {|[a,d]|}

proof end;

theorem Th45: :: JGRAPH_6:45

{ q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = 1 & - 1 <= p `1 & p `1 <= 1 ) or ( p `1 = 1 & - 1 <= p `2 & p `2 <= 1 ) or ( p `2 = - 1 & - 1 <= p `1 & p `1 <= 1 ) ) }

proof end;

theorem Th46: :: JGRAPH_6:46

for a, b, c, d being real number st a <= b & c <= d holds
W-bound (rectangle a,b,c,d) = a

proof end;

theorem Th47: :: JGRAPH_6:47

for a, b, c, d being real number st a <= b & c <= d holds
N-bound (rectangle a,b,c,d) = d

proof end;

theorem Th48: :: JGRAPH_6:48

for a, b, c, d being real number st a <= b & c <= d holds
E-bound (rectangle a,b,c,d) = b

proof end;

theorem Th49: :: JGRAPH_6:49

for a, b, c, d being real number st a <= b & c <= d holds
S-bound (rectangle a,b,c,d) = c

proof end;

theorem Th50: :: JGRAPH_6:50

for a, b, c, d being real number st a <= b & c <= d holds
NW-corner (rectangle a,b,c,d) = |[a,d]|

proof end;

theorem Th51: :: JGRAPH_6:51

for a, b, c, d being real number st a <= b & c <= d holds
NE-corner (rectangle a,b,c,d) = |[b,d]|

proof end;

theorem :: JGRAPH_6:52

for a, b, c, d being real number st a <= b & c <= d holds
SW-corner (rectangle a,b,c,d) = |[a,c]|

proof end;

theorem :: JGRAPH_6:53

for a, b, c, d being real number st a <= b & c <= d holds
SE-corner (rectangle a,b,c,d) = |[b,c]|

proof end;

theorem Th54: :: JGRAPH_6:54

for a, b, c, d being real number st a <= b & c <= d holds
W-most (rectangle a,b,c,d) = LSeg |[a,c]|,|[a,d]|

proof end;

theorem Th55: :: JGRAPH_6:55

for a, b, c, d being real number st a <= b & c <= d holds
E-most (rectangle a,b,c,d) = LSeg |[b,c]|,|[b,d]|

proof end;

theorem Th56: :: JGRAPH_6:56

for a, b, c, d being real number st a <= b & c <= d holds
( W-min (rectangle a,b,c,d) = |[a,c]| & E-max (rectangle a,b,c,d) = |[b,d]| )

proof end;

theorem Th57: :: JGRAPH_6:57

for a, b, c, d being real number st a < b & c < d holds
( (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|) is_an_arc_of W-min (rectangle a,b,c,d), E-max (rectangle a,b,c,d) & (LSeg |[a,c]|,|[b,c]|) \/ (LSeg |[b,c]|,|[b,d]|) is_an_arc_of E-max (rectangle a,b,c,d), W-min (rectangle a,b,c,d) )

proof end;

theorem Th58: :: JGRAPH_6:58

for a, b, c, d being real number
for f1, f2 being FinSequence of (TOP-REAL 2)
for p0, p1, p01, p10 being Point of (TOP-REAL 2) st a & f2 = <*p0,p10,p1*> holds
( f1 is_S-Seq & L~ f1 = (LSeg p0,p01) \/ (LSeg p01,p1) & f2 is_S-Seq & L~ f2 = (LSeg p0,p10) \/ (LSeg p10,p1) & rectangle a,b,c,d = (L~ f1) \/ (L~ f2) & (L~ f1) /\ (L~ f2) = {p0,p1} & f1 /. 1 = p0 & f1 /. (len f1) = p1 & f2 /. 1 = p0 & f2 /. (len f2) = p1 )

proof end;

theorem Th59: :: JGRAPH_6:59

for P1, P2 being Subset of (TOP-REAL 2)
for a, b, c, d being real number
for f1, f2 being FinSequence of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st a & f2 = <*|[a,c]|,|[b,c]|,|[b,d]|*> & P1 = L~ f1 & P2 = L~ f2 holds
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & not P1 is empty & not P2 is empty & rectangle a,b,c,d = P1 \/ P2 & P1 /\ P2 = {p1,p2} )

proof end;

theorem Th60: :: JGRAPH_6:60

for a, b, c, d being real number st a < b & c < d holds
rectangle a,b,c,d is_simple_closed_curve

proof end;

theorem Th61: :: JGRAPH_6:61

for a, b, c, d being real number st a < b & c < d holds
Upper_Arc (rectangle a,b,c,d) = (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|)

proof end;

theorem Th62: :: JGRAPH_6:62

for a, b, c, d being real number st a < b & c < d holds
Lower_Arc (rectangle a,b,c,d) = (LSeg |[a,c]|,|[b,c]|) \/ (LSeg |[b,c]|,|[b,d]|)

proof end;

theorem Th63: :: JGRAPH_6:63

for a, b, c, d being real number st a < b & c < d holds
ex f being Function of I[01] ,((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) st
( f is_homeomorphism & f . 0 = W-min (rectangle a,b,c,d) & f . 1 = E-max (rectangle a,b,c,d) & rng f = Upper_Arc (rectangle a,b,c,d) & ( for r being Real st r in [.0,(1 / 2).] holds
f . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) ) & ( for r being Real st r in [.(1 / 2),1.] holds
f . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) ) & ( for p being Point of (TOP-REAL 2) st p in LSeg |[a,c]|,|[a,d]| holds
( 0 <= (((p `2 ) - c) / (d - c)) / 2 & (((p `2 ) - c) / (d - c)) / 2 <= 1 & f . ((((p `2 ) - c) / (d - c)) / 2) = p ) ) & ( for p being Point of (TOP-REAL 2) st p in LSeg |[a,d]|,|[b,d]| holds
( 0 <= ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) & ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) <= 1 & f . (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2)) = p ) ) )

proof end;

theorem Th64: :: JGRAPH_6:64

for a, b, c, d being real number st a < b & c < d holds
ex f being Function of I[01] ,((TOP-REAL 2) | (Lower_Arc (rectangle a,b,c,d))) st
( f is_homeomorphism & f . 0 = E-max (rectangle a,b,c,d) & f . 1 = W-min (rectangle a,b,c,d) & rng f = Lower_Arc (rectangle a,b,c,d) & ( for r being Real st r in [.0,(1 / 2).] holds
f . r = ((1 - (2 * r)) * |[b,d]|) + ((2 * r) * |[b,c]|) ) & ( for r being Real st r in [.(1 / 2),1.] holds
f . r = ((1 - ((2 * r) - 1)) * |[b,c]|) + (((2 * r) - 1) * |[a,c]|) ) & ( for p being Point of (TOP-REAL 2) st p in LSeg |[b,d]|,|[b,c]| holds
( 0 <= (((p `2 ) - d) / (c - d)) / 2 & (((p `2 ) - d) / (c - d)) / 2 <= 1 & f . ((((p `2 ) - d) / (c - d)) / 2) = p ) ) & ( for p being Point of (TOP-REAL 2) st p in LSeg |[b,c]|,|[a,c]| holds
( 0 <= ((((p `1 ) - b) / (a - b)) / 2) + (1 / 2) & ((((p `1 ) - b) / (a - b)) / 2) + (1 / 2) <= 1 & f . (((((p `1 ) - b) / (a - b)) / 2) + (1 / 2)) = p ) ) )

proof end;

theorem Th65: :: JGRAPH_6:65

for a, b, c, d being real number
for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg |[a,c]|,|[a,d]| & p2 in LSeg |[a,c]|,|[a,d]| holds
( LE p1,p2, rectangle a,b,c,d iff p1 `2 <= p2 `2 )

proof end;

theorem Th66: :: JGRAPH_6:66

for a, b, c, d being real number
for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg |[a,d]|,|[b,d]| & p2 in LSeg |[a,d]|,|[b,d]| holds
( LE p1,p2, rectangle a,b,c,d iff p1 `1 <= p2 `1 )

proof end;

theorem Th67: :: JGRAPH_6:67

for a, b, c, d being real number
for p1, p2 being Point of (TOP-REAL 2) st a = p2 `2 )

proof end;

theorem Th68: :: JGRAPH_6:68

for a, b, c, d being real number
for p1, p2 being Point of (TOP-REAL 2) st a W-min (rectangle a,b,c,d) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) )

proof end;

theorem Th69: :: JGRAPH_6:69

for a, b, c, d being real number
for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg |[a,c]|,|[a,d]| holds
( LE p1,p2, rectangle a,b,c,d iff ( ( p2 in LSeg |[a,c]|,|[a,d]| & p1 `2 <= p2 `2 ) or p2 in LSeg |[a,d]|,|[b,d]| or p2 in LSeg |[b,d]|,|[b,c]| or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ) )

proof end;

theorem Th70: :: JGRAPH_6:70

for a, b, c, d being real number
for p1, p2 being Point of (TOP-REAL 2) st a W-min (rectangle a,b,c,d) ) ) )

proof end;

theorem Th71: :: JGRAPH_6:71

for a, b, c, d being real number
for p1, p2 being Point of (TOP-REAL 2) st a = p2 `2 ) or ( p2 in LSeg |[b,c]|,|[a,c]| & p2 <> W-min (rectangle a,b,c,d) ) ) )

proof end;

theorem Th72: :: JGRAPH_6:72

for a, b, c, d being real number
for p1, p2 being Point of (TOP-REAL 2) st a W-min (rectangle a,b,c,d) holds
( LE p1,p2, rectangle a,b,c,d iff ( p2 in LSeg |[b,c]|,|[a,c]| & p1 `1 >= p2 `1 & p2 <> W-min (rectangle a,b,c,d) ) )

proof end;

theorem Th73: :: JGRAPH_6:73

for x being set
for a, b, c, d being real number st x in rectangle a,b,c,d & a < b & c < d & not x in LSeg |[a,c]|,|[a,d]| & not x in LSeg |[a,d]|,|[b,d]| & not x in LSeg |[b,d]|,|[b,c]| holds
x in LSeg |[b,c]|,|[a,c]|

proof end;

theorem Th74: :: JGRAPH_6:74

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

proof end;

theorem Th75: :: JGRAPH_6:75

for p1, p2 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle 0,0,1 & f = Sq_Circ & p1 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & p1 `2 >= 0 & LE p1,p2, rectangle (- 1),1,(- 1),1 holds
LE f . p1,f . p2,P

proof end;

theorem Th76: :: JGRAPH_6:76

for p1, p2, p3 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle 0,0,1 & f = Sq_Circ & p1 in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & p1 `2 >= 0 & LE p1,p2, rectangle (- 1),1,(- 1),1 & LE p2,p3, rectangle (- 1),1,(- 1),1 holds
LE f . p2,f . p3,P

proof end;

theorem Th77: :: JGRAPH_6:77

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

proof end;

theorem Th78: :: JGRAPH_6:78

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

proof end;

theorem Th79: :: JGRAPH_6:79

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

proof end;

theorem Th80: :: JGRAPH_6:80

for p, q being Point of (TOP-REAL 2)
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ & p in LSeg |[(- 1),(- 1)]|,|[(- 1),1]| & q in LSeg |[1,(- 1)]|,|[(- 1),(- 1)]| holds
(f . p) `1 <= (f . q) `1

proof end;

theorem Th81: :: JGRAPH_6:81

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

proof end;

theorem Th82: :: JGRAPH_6:82

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle 0,0,1 & f = Sq_Circ & LE p1,p2, rectangle (- 1),1,(- 1),1 & LE p2,p3, rectangle (- 1),1,(- 1),1 & LE p3,p4, rectangle (- 1),1,(- 1),1 holds
f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P

proof end;

theorem Th83: :: JGRAPH_6:83

for p1, p2 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2) st P is_simple_closed_curve & p1 in P & p2 in P & not LE p1,p2,P holds
LE p2,p1,P

proof end;

theorem :: JGRAPH_6:84

for p1, p2, p3 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2) st P is_simple_closed_curve & p1 in P & p2 in P & p3 in P & not ( LE p1,p2,P & LE p2,p3,P ) & not ( LE p1,p3,P & LE p3,p2,P ) & not ( LE p2,p1,P & LE p1,p3,P ) & not ( LE p2,p3,P & LE p3,p1,P ) & not ( LE p3,p1,P & LE p1,p2,P ) holds
( LE p3,p2,P & LE p2,p1,P ) by Th83;

theorem :: JGRAPH_6:85

for p1, p2, p3 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2) st P is_simple_closed_curve & p1 in P & p2 in P & p3 in P & LE p2,p3,P & not LE p1,p2,P & not ( LE p2,p1,P & LE p1,p3,P ) holds
LE p3,p1,P by Th83;

theorem :: JGRAPH_6:86

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2) st P is_simple_closed_curve & p1 in P & p2 in P & p3 in P & p4 in P & LE p2,p3,P & LE p3,p4,P & not LE p1,p2,P & not ( LE p2,p1,P & LE p1,p3,P ) & not ( LE p3,p1,P & LE p1,p4,P ) holds
LE p4,p1,P by Th83;

theorem Th87: :: JGRAPH_6:87

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle 0,0,1 & f = Sq_Circ & LE f . p1,f . p2,P & LE f . p2,f . p3,P & LE f . p3,f . p4,P holds
p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1

proof end;

theorem Th88: :: JGRAPH_6:88

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for P being non empty compact Subset of (TOP-REAL 2)
for f being Function of (TOP-REAL 2),(TOP-REAL 2) st P = circle 0,0,1 & f = Sq_Circ holds
( p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 iff f . p1,f . p2,f . p3,f . p4 are_in_this_order_on P )

proof end;

theorem :: JGRAPH_6:89

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for K0 being Subset of (TOP-REAL 2) st p1,p2,p3,p4 are_in_this_order_on rectangle (- 1),1,(- 1),1 holds
for f, g being Function of I[01] ,(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & K0 = closed_inside_of_rectangle (- 1),1,(- 1),1 & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= K0 & rng g c= K0 holds
rng f meets rng g

proof end;