:: by Yatsuka Nakamura

::

:: Received February 25, 2003

:: Copyright (c) 2003-2021 Association of Mizar Users

Lm1: for a, b being Real st b <= 0 & a <= b holds

a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))

proof end;

Lm2: for a, b being Real st a <= 0 & a <= b holds

a * (sqrt (1 + (b ^2))) <= b * (sqrt (1 + (a ^2)))

proof end;

Lm3: for a, b being Real st a >= 0 & a >= b holds

a * (sqrt (1 + (b ^2))) >= b * (sqrt (1 + (a ^2)))

proof end;

theorem Th1: :: JGRAPH_6:1

for a, c, d being Real

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 )

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 Th2: :: JGRAPH_6:2

for a, c, d being Real

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]|)

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 Th3: :: JGRAPH_6:3

for a, b, d being Real

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 )

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 Th5: :: JGRAPH_6:5

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 )

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

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 )

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 Th7: :: JGRAPH_6:7

for X being non empty TopSpace

for f1 being Function of X,R^1

for a being Real st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 - a ) & g is continuous )

for f1 being Function of X,R^1

for a being Real st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = r1 - a ) & g is continuous )

proof end;

theorem Th8: :: JGRAPH_6:8

for X being non empty TopSpace

for f1 being Function of X,R^1

for a being Real st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = a - r1 ) & g is continuous )

for f1 being Function of X,R^1

for a being Real st f1 is continuous holds

ex g being Function of X,R^1 st

( ( for p being Point of X

for r1 being Real st f1 . p = r1 holds

g . p = a - r1 ) & g is continuous )

proof end;

theorem Th9: :: JGRAPH_6:9

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 )

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 :: JGRAPH_6:11

theorem Th12: :: JGRAPH_6:12

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 )

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 Th13: :: JGRAPH_6:13

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 )

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;

Lm4: |[(- 1),0]| `1 = - 1

by EUCLID:52;

Lm5: |[(- 1),0]| `2 = 0

by EUCLID:52;

Lm6: |[1,0]| `1 = 1

by EUCLID:52;

Lm7: |[1,0]| `2 = 0

by EUCLID:52;

Lm8: |[0,(- 1)]| `1 = 0

by EUCLID:52;

Lm9: |[0,(- 1)]| `2 = - 1

by EUCLID:52;

Lm10: |[0,1]| `1 = 0

by EUCLID:52;

Lm11: |[0,1]| `2 = 1

by EUCLID:52;

Lm12: now :: thesis: ( |.|[(- 1),0]|.| = 1 & |.|[1,0]|.| = 1 & |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )

thus |.|[(- 1),0]|.| =
sqrt (((- 1) ^2) + (0 ^2))
by Lm4, Lm5, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: ( |.|[1,0]|.| = 1 & |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )

thus |.|[1,0]|.| = sqrt ((1 ^2) + (0 ^2)) by Lm6, Lm7, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: ( |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )

thus |.|[0,(- 1)]|.| = sqrt ((0 ^2) + ((- 1) ^2)) by Lm8, Lm9, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: |.|[0,1]|.| = 1

thus |.|[0,1]|.| = sqrt ((0 ^2) + (1 ^2)) by Lm10, Lm11, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: verum

end;
.= 1 by SQUARE_1:18 ; :: thesis: ( |.|[1,0]|.| = 1 & |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )

thus |.|[1,0]|.| = sqrt ((1 ^2) + (0 ^2)) by Lm6, Lm7, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: ( |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )

thus |.|[0,(- 1)]|.| = sqrt ((0 ^2) + ((- 1) ^2)) by Lm8, Lm9, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: |.|[0,1]|.| = 1

thus |.|[0,1]|.| = sqrt ((0 ^2) + (1 ^2)) by Lm10, Lm11, JGRAPH_3:1

.= 1 by SQUARE_1:18 ; :: thesis: verum

Lm13: 0 in [.0,1.]

by XXREAL_1:1;

Lm14: 1 in [.0,1.]

by XXREAL_1:1;

theorem Th14: :: JGRAPH_6:14

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

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 Th15: :: JGRAPH_6:15

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

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 Th16: :: JGRAPH_6:16

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

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 Th17: :: JGRAPH_6:17

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

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 Th18: :: JGRAPH_6:18

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

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;

Lm15: for a, b, c, d being Real 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 Th19: :: JGRAPH_6:19

for a, b, c, d being Real

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 )

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;

{ p where p is Point of (TOP-REAL 2) : ( a < p `1 & p `1 < b & c < p `2 & p `2 < d ) } is Subset of (TOP-REAL 2)

end;
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 { p where p is Point of (TOP-REAL 2) : ( a < p `1 & p `1 < b & c < p `2 & p `2 < d ) } ;

{ p where p is Point of (TOP-REAL 2) : ( a < p `1 & p `1 < b & c < p `2 & p `2 < d ) } is Subset of (TOP-REAL 2)

proof end;

:: deftheorem defines inside_of_rectangle JGRAPH_6:def 1 :

for a, b, c, d being Real holds inside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( a < p `1 & p `1 < b & c < p `2 & p `2 < d ) } ;

for a, b, c, d being Real holds inside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( a < p `1 & p `1 < b & c < p `2 & p `2 < d ) } ;

definition

let a, b, c, d be Real;

{ p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } is Subset of (TOP-REAL 2)

end;
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 { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } ;

{ p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } is Subset of (TOP-REAL 2)

proof end;

:: deftheorem defines closed_inside_of_rectangle JGRAPH_6:def 2 :

for a, b, c, d being Real holds closed_inside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } ;

for a, b, c, d being Real holds closed_inside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) } ;

definition

let a, b, c, d be Real;

{ 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 ) } is Subset of (TOP-REAL 2)

end;
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 { 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 ) } ;

{ 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 ) } is Subset of (TOP-REAL 2)

proof end;

:: deftheorem defines outside_of_rectangle JGRAPH_6:def 3 :

for a, b, c, d being Real holds outside_of_rectangle (a,b,c,d) = { 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 ) } ;

for a, b, c, d being Real holds outside_of_rectangle (a,b,c,d) = { 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 ) } ;

definition

let a, b, c, d be Real;

{ 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 ) } is Subset of (TOP-REAL 2)

end;
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 { 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 ) } ;

{ 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 ) } is Subset of (TOP-REAL 2)

proof end;

:: deftheorem defines closed_outside_of_rectangle JGRAPH_6:def 4 :

for a, b, c, d being Real holds closed_outside_of_rectangle (a,b,c,d) = { 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 ) } ;

for a, b, c, d being Real holds closed_outside_of_rectangle (a,b,c,d) = { 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 ) } ;

theorem Th20: :: JGRAPH_6:20

for a, b, r being Real

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

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 Th21: :: JGRAPH_6:21

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 being_homeomorphism & P is being_simple_closed_curve holds

Q is being_simple_closed_curve

Q is being_simple_closed_curve

proof end;

theorem Th23: :: JGRAPH_6:23

for a, b, r being Real

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 being_simple_closed_curve

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 being_simple_closed_curve

proof end;

definition

let a, b, r be Real;

{ p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } is Subset of (TOP-REAL 2)

end;
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 { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } ;

{ p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } is Subset of (TOP-REAL 2)

proof end;

:: deftheorem defines circle JGRAPH_6:def 5 :

for a, b, r being Real holds circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } ;

for a, b, r being Real holds circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } ;

registration
end;

definition

let a, b, r be Real;

{ p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| < r } is Subset of (TOP-REAL 2)

end;
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 { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| < r } ;

{ p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| < r } is Subset of (TOP-REAL 2)

proof end;

:: deftheorem defines inside_of_circle JGRAPH_6:def 6 :

for a, b, r being Real holds inside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| < r } ;

for a, b, r being Real holds inside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| < r } ;

definition

let a, b, r be Real;

{ p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| <= r } is Subset of (TOP-REAL 2)

end;
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 { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| <= r } ;

{ p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| <= r } is Subset of (TOP-REAL 2)

proof end;

:: deftheorem defines closed_inside_of_circle JGRAPH_6:def 7 :

for a, b, r being Real holds closed_inside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| <= r } ;

for a, b, r being Real holds closed_inside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| <= r } ;

definition

let a, b, r be Real;

{ p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| > r } is Subset of (TOP-REAL 2)

end;
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 { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| > r } ;

{ p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| > r } is Subset of (TOP-REAL 2)

proof end;

:: deftheorem defines outside_of_circle JGRAPH_6:def 8 :

for a, b, r being Real holds outside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| > r } ;

for a, b, r being Real holds outside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| > r } ;

definition

let a, b, r be Real;

{ p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| >= r } is Subset of (TOP-REAL 2)

end;
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 { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| >= r } ;

{ p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| >= r } is Subset of (TOP-REAL 2)

proof end;

:: deftheorem defines closed_outside_of_circle JGRAPH_6:def 9 :

for a, b, r being Real holds closed_outside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| >= r } ;

for a, b, r being Real holds closed_outside_of_circle (a,b,r) = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| >= r } ;

theorem Th24: :: JGRAPH_6:24

for r being Real 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 } )

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

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

Sq_Circ .: Kb = Cb

proof end;

theorem Th26: :: JGRAPH_6:26

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

Sq_Circ .: Kb = Cb

proof end;

theorem Th27: :: JGRAPH_6:27

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

Sq_Circ .: Kb = Cb

proof end;

theorem Th28: :: JGRAPH_6:28

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

Sq_Circ .: Kb = Cb

proof end;

theorem :: JGRAPH_6:29

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 )

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 Th30: :: JGRAPH_6:30

for a, b, c, d being Real 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 ) } )

( 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 Th31: :: JGRAPH_6:31

for a, b, c, d being Real st a <= b & c <= d holds

(LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) = {|[a,c]|}

(LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,c]|,|[b,c]|)) = {|[a,c]|}

proof end;

theorem Th32: :: JGRAPH_6:32

for a, b, c, d being Real st a <= b & c <= d holds

(LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,c]|}

(LSeg (|[a,c]|,|[b,c]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,c]|}

proof end;

theorem Th33: :: JGRAPH_6:33

for a, b, c, d being Real st a <= b & c <= d holds

(LSeg (|[a,d]|,|[b,d]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,d]|}

(LSeg (|[a,d]|,|[b,d]|)) /\ (LSeg (|[b,c]|,|[b,d]|)) = {|[b,d]|}

proof end;

theorem Th34: :: JGRAPH_6:34

for a, b, c, d being Real st a <= b & c <= d holds

(LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,d]|,|[b,d]|)) = {|[a,d]|}

(LSeg (|[a,c]|,|[a,d]|)) /\ (LSeg (|[a,d]|,|[b,d]|)) = {|[a,d]|}

proof end;

theorem Th35: :: JGRAPH_6:35

{ 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 Th44: :: JGRAPH_6:44

for a, b, c, d being Real st a <= b & c <= d holds

W-most (rectangle (a,b,c,d)) = LSeg (|[a,c]|,|[a,d]|)

W-most (rectangle (a,b,c,d)) = LSeg (|[a,c]|,|[a,d]|)

proof end;

theorem Th45: :: JGRAPH_6:45

for a, b, c, d being Real st a <= b & c <= d holds

E-most (rectangle (a,b,c,d)) = LSeg (|[b,c]|,|[b,d]|)

E-most (rectangle (a,b,c,d)) = LSeg (|[b,c]|,|[b,d]|)

proof end;

theorem Th46: :: JGRAPH_6:46

for a, b, c, d being Real st a <= b & c <= d holds

( W-min (rectangle (a,b,c,d)) = |[a,c]| & E-max (rectangle (a,b,c,d)) = |[b,d]| )

( W-min (rectangle (a,b,c,d)) = |[a,c]| & E-max (rectangle (a,b,c,d)) = |[b,d]| )

proof end;

theorem Th47: :: JGRAPH_6:47

for a, b, c, d being Real 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)) )

( (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 Th48: :: JGRAPH_6:48

for a, b, c, d being Real

for f1, f2 being FinSequence of (TOP-REAL 2)

for p0, p1, p01, p10 being Point of (TOP-REAL 2) st a < b & c < d & p0 = |[a,c]| & p1 = |[b,d]| & p01 = |[a,d]| & p10 = |[b,c]| & f1 = <*p0,p01,p1*> & f2 = <*p0,p10,p1*> holds

( f1 is being_S-Seq & L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) & f2 is being_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 )

for f1, f2 being FinSequence of (TOP-REAL 2)

for p0, p1, p01, p10 being Point of (TOP-REAL 2) st a < b & c < d & p0 = |[a,c]| & p1 = |[b,d]| & p01 = |[a,d]| & p10 = |[b,c]| & f1 = <*p0,p01,p1*> & f2 = <*p0,p10,p1*> holds

( f1 is being_S-Seq & L~ f1 = (LSeg (p0,p01)) \/ (LSeg (p01,p1)) & f2 is being_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 Th49: :: JGRAPH_6:49

for P1, P2 being Subset of (TOP-REAL 2)

for a, b, c, d being Real

for f1, f2 being FinSequence of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 = |[a,c]| & p2 = |[b,d]| & f1 = <*|[a,c]|,|[a,d]|,|[b,d]|*> & 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} )

for a, b, c, d being Real

for f1, f2 being FinSequence of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 = |[a,c]| & p2 = |[b,d]| & f1 = <*|[a,c]|,|[a,d]|,|[b,d]|*> & 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 Th51: :: JGRAPH_6:51

for a, b, c, d being Real st a < b & c < d holds

Upper_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))

Upper_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[a,d]|)) \/ (LSeg (|[a,d]|,|[b,d]|))

proof end;

theorem Th52: :: JGRAPH_6:52

for a, b, c, d being Real st a < b & c < d holds

Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|))

Lower_Arc (rectangle (a,b,c,d)) = (LSeg (|[a,c]|,|[b,c]|)) \/ (LSeg (|[b,c]|,|[b,d]|))

proof end;

theorem Th53: :: JGRAPH_6:53

for a, b, c, d being Real 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 being_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 ) ) )

ex f being Function of I[01],((TOP-REAL 2) | (Upper_Arc (rectangle (a,b,c,d)))) st

( f is being_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 Th54: :: JGRAPH_6:54

for a, b, c, d being Real 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 being_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 ) ) )

ex f being Function of I[01],((TOP-REAL 2) | (Lower_Arc (rectangle (a,b,c,d)))) st

( f is being_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 Th55: :: JGRAPH_6:55

for a, b, c, d being Real

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 )

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 Th56: :: JGRAPH_6:56

for a, b, c, d being Real

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 )

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 Th57: :: JGRAPH_6:57

for a, b, c, d being Real

for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[b,c]|,|[b,d]|) & p2 in LSeg (|[b,c]|,|[b,d]|) holds

( LE p1,p2, rectangle (a,b,c,d) iff p1 `2 >= p2 `2 )

for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[b,c]|,|[b,d]|) & p2 in LSeg (|[b,c]|,|[b,d]|) holds

( LE p1,p2, rectangle (a,b,c,d) iff p1 `2 >= p2 `2 )

proof end;

theorem Th58: :: JGRAPH_6:58

for a, b, c, d being Real

for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[a,c]|,|[b,c]|) & p2 in LSeg (|[a,c]|,|[b,c]|) holds

( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) )

for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[a,c]|,|[b,c]|) & p2 in LSeg (|[a,c]|,|[b,c]|) holds

( LE p1,p2, rectangle (a,b,c,d) & p1 <> W-min (rectangle (a,b,c,d)) iff ( p1 `1 >= p2 `1 & p2 <> W-min (rectangle (a,b,c,d)) ) )

proof end;

theorem Th59: :: JGRAPH_6:59

for a, b, c, d being Real

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

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 Th60: :: JGRAPH_6:60

for a, b, c, d being Real

for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[a,d]|,|[b,d]|) holds

( LE p1,p2, rectangle (a,b,c,d) iff ( ( p2 in LSeg (|[a,d]|,|[b,d]|) & p1 `1 <= p2 `1 ) or p2 in LSeg (|[b,d]|,|[b,c]|) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) )

for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[a,d]|,|[b,d]|) holds

( LE p1,p2, rectangle (a,b,c,d) iff ( ( p2 in LSeg (|[a,d]|,|[b,d]|) & p1 `1 <= p2 `1 ) 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 Th61: :: JGRAPH_6:61

for a, b, c, d being Real

for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[b,d]|,|[b,c]|) holds

( LE p1,p2, rectangle (a,b,c,d) iff ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) )

for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[b,d]|,|[b,c]|) holds

( LE p1,p2, rectangle (a,b,c,d) iff ( ( p2 in LSeg (|[b,d]|,|[b,c]|) & p1 `2 >= p2 `2 ) or ( p2 in LSeg (|[b,c]|,|[a,c]|) & p2 <> W-min (rectangle (a,b,c,d)) ) ) )

proof end;

theorem Th62: :: JGRAPH_6:62

for a, b, c, d being Real

for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[b,c]|,|[a,c]|) & p1 <> 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)) ) )

for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg (|[b,c]|,|[a,c]|) & p1 <> 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 Th63: :: JGRAPH_6:63

for x being set

for a, b, c, d being Real 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]|)

for a, b, c, d being Real 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 Th64: :: JGRAPH_6:64

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)]| )

( p2 in LSeg (|[1,(- 1)]|,|[(- 1),(- 1)]|) & p2 <> |[(- 1),(- 1)]| )

proof end;

theorem Th65: :: JGRAPH_6:65

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

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 Th66: :: JGRAPH_6:66

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

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 Th67: :: JGRAPH_6:67

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 )

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 Th68: :: JGRAPH_6:68

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 f = Sq_Circ holds

( (f . p) `1 >= 0 iff p `1 >= 0 )

for P being non empty compact Subset of (TOP-REAL 2)

for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ holds

( (f . p) `1 >= 0 iff p `1 >= 0 )

proof end;

theorem Th69: :: JGRAPH_6:69

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 f = Sq_Circ holds

( (f . p) `2 >= 0 iff p `2 >= 0 )

for P being non empty compact Subset of (TOP-REAL 2)

for f being Function of (TOP-REAL 2),(TOP-REAL 2) st f = Sq_Circ holds

( (f . p) `2 >= 0 iff p `2 >= 0 )

proof end;

theorem Th70: :: JGRAPH_6:70

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

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 Th71: :: JGRAPH_6:71

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

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 Th72: :: JGRAPH_6:72

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

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 Th73: :: JGRAPH_6:73

for p1, p2 being Point of (TOP-REAL 2)

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

LE p2,p1,P

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

LE p2,p1,P

proof end;

theorem :: JGRAPH_6:74

for p1, p2, p3 being Point of (TOP-REAL 2)

for P being non empty compact Subset of (TOP-REAL 2) st P is being_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 Th73;

for P being non empty compact Subset of (TOP-REAL 2) st P is being_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 Th73;

theorem :: JGRAPH_6:75

theorem :: JGRAPH_6:76

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 being_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 Th73;

for P being non empty compact Subset of (TOP-REAL 2) st P is being_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 Th73;

theorem Th77: :: JGRAPH_6:77

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)

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 Th78: :: JGRAPH_6:78

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 )

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:79

for p1, p2, p3, p4 being Point 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 & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= closed_inside_of_rectangle ((- 1),1,(- 1),1) & rng g c= closed_inside_of_rectangle ((- 1),1,(- 1),1) holds

rng f meets rng g

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

rng f meets rng g

proof end;