:: General {F}ashoda Meet Theorem for Unit Circle and Square
:: 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 )

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

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 )

proof end;

theorem Th4: :: JGRAPH_6:4

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

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 )

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 )

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 )

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 )

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 )

proof end;

theorem Th10: :: JGRAPH_6:10

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

proof end;

theorem :: JGRAPH_6:11

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 Th10, JGRAPH_5:29;

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 )

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 )

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;

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

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

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

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

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

proof end;

notation

let a, b, c, d be Real;
synonym rectangle (a,b,c,d) for [.a,b,c,d.];

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 )

proof end;

definition

let a, b, c, d be Real;

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

proof end;

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

definition

let a, b, c, d be Real;

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

proof end;

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

definition

let a, b, c, d be Real;

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

proof end;

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

definition

let a, b, c, d be Real;

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

proof end;

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

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

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

proof end;

theorem Th22: :: JGRAPH_6:22

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

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

proof end;

definition

let a, b, r be Real;

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

proof end;

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 } ;

registration

let a, b, r be Real;

cluster circle (a,b,r) -> compact ;

coherence
circle (a,b,r) is compact

proof end;

end;

registration

let a, b be Real;
let r be non negative Real;

cluster circle (a,b,r) -> non empty ;

coherence
not circle (a,b,r) is empty

proof end;

end;

definition

let a, b, r be Real;

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

proof end;

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 } ;

definition

let a, b, r be Real;

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

proof end;

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 } ;

definition

let a, b, r be Real;

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

proof end;

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 } ;

definition

let a, b, r be Real;

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

proof end;

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 } ;

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

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

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

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

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

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 )

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

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

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

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

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

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 Th36: :: JGRAPH_6:36

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

proof end;

theorem Th37: :: JGRAPH_6:37

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

proof end;

theorem Th38: :: JGRAPH_6:38

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

proof end;

theorem Th39: :: JGRAPH_6:39

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

proof end;

theorem Th40: :: JGRAPH_6:40

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

proof end;

theorem Th41: :: JGRAPH_6:41

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

proof end;

theorem :: JGRAPH_6:42

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

proof end;

theorem :: JGRAPH_6:43

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

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

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

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

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

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 )

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

proof end;

theorem Th50: :: JGRAPH_6:50

for a, b, c, d being Real st a < b & c < d holds
rectangle (a,b,c,d) is being_simple_closed_curve

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

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

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

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

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 )

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 )

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 )

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

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

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

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

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

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

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

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

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

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 )

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 )

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 )

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

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

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

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

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;

theorem :: JGRAPH_6:75

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 & LE p2,p3,P & not LE p1,p2,P & not ( LE p2,p1,P & LE p1,p3,P ) holds
LE p3,p1,P by Th73;

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;

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)

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 )

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

proof end;