:: JORDAN semantic presentation

set T2 = TOP-REAL 2;

Lm1: for A, B, C, Z being set st A c= Z & B c= Z & C c= Z holds
(A \/ B) \/ C c= Z

proof end;

Lm2: for A, B, C, D, Z being set st A c= Z & B c= Z & C c= Z & D c= Z holds
((A \/ B) \/ C) \/ D c= Z

proof end;

Lm3: for A, B, C, D, Z being set st A misses Z & B misses Z & C misses Z & D misses Z holds
((A \/ B) \/ C) \/ D misses Z

proof end;

registration

let M be Reflexive symmetric triangle MetrStruct ;
let x, y be Point of M;
cluster dist x,y -> non negative ;
coherence by METRIC_1:5;

end;

registration

let n be Nat;
let x, y be Point of (TOP-REAL n);
cluster dist x,y -> non negative ;
coherence

proof end;

end;

registration

let n be Nat;
let x, y be Point of (TOP-REAL n);
cluster |.(x - y).| -> non negative ;
coherence

proof end;

end;

theorem Th1: :: JORDAN:1

for n being Nat
for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
(1 / 2) * (p1 + p2) <> p1

proof end;

theorem Th2: :: JORDAN:2

for p1, p2 being Point of (TOP-REAL 2) st p1 `2 < p2 `2 holds
p1 `2 < ((1 / 2) * (p1 + p2)) `2

proof end;

theorem Th3: :: JORDAN:3

for p1, p2 being Point of (TOP-REAL 2) st p1 `2 < p2 `2 holds
((1 / 2) * (p1 + p2)) `2 < p2 `2

proof end;

theorem Th4: :: JORDAN:4

for B being Subset of (TOP-REAL 2)
for A being vertical Subset of (TOP-REAL 2) holds A /\ B is vertical

proof end;

theorem :: JORDAN:5

for B being Subset of (TOP-REAL 2)
for A being horizontal Subset of (TOP-REAL 2) holds A /\ B is horizontal

proof end;

theorem :: JORDAN:6

for p, p1, p2 being Point of (TOP-REAL 2) st p in LSeg p1,p2 & LSeg p1,p2 is vertical holds
LSeg p,p2 is vertical

proof end;

theorem :: JORDAN:7

for p, p1, p2 being Point of (TOP-REAL 2) st p in LSeg p1,p2 & LSeg p1,p2 is horizontal holds
LSeg p,p2 is horizontal

proof end;

registration

let P be Subset of (TOP-REAL 2);
cluster LSeg (SW-corner P),(SE-corner P) -> horizontal ;
coherence

proof end;

cluster LSeg (NW-corner P),(SW-corner P) -> vertical ;
coherence

proof end;

cluster LSeg (NE-corner P),(SE-corner P) -> vertical ;
coherence

proof end;

end;

registration

let P be Subset of (TOP-REAL 2);
cluster LSeg (SE-corner P),(SW-corner P) -> horizontal ;
coherence ;
cluster LSeg (SW-corner P),(NW-corner P) -> vertical ;
coherence ;
cluster LSeg (SE-corner P),(NE-corner P) -> vertical ;
coherence ;

end;

registration

cluster non empty compact vertical -> with_the_max_arc Element of bool the carrier of (TOP-REAL 2);
coherence

proof end;

end;

theorem Th8: :: JORDAN:8

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( W-min Y in X or W-max Y in X ) holds
W-bound X = W-bound Y

proof end;

theorem Th9: :: JORDAN:9

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( E-min Y in X or E-max Y in X ) holds
E-bound X = E-bound Y

proof end;

theorem :: JORDAN:10

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( N-min Y in X or N-max Y in X ) holds
N-bound X = N-bound Y

proof end;

theorem :: JORDAN:11

for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & ( S-min Y in X or S-max Y in X ) holds
S-bound X = S-bound Y

proof end;

theorem :: JORDAN:12

for C being Simple_closed_curve holds W-bound C = W-bound (North_Arc C)

proof end;

theorem :: JORDAN:13

for C being Simple_closed_curve holds E-bound C = E-bound (North_Arc C)

proof end;

theorem :: JORDAN:14

for C being Simple_closed_curve holds W-bound C = W-bound (South_Arc C)

proof end;

theorem :: JORDAN:15

for C being Simple_closed_curve holds E-bound C = E-bound (South_Arc C)

proof end;

theorem Th16: :: JORDAN:16

for r being real number
for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= r & r <= p2 `1 holds
LSeg p1,p2 meets Vertical_Line r

proof end;

theorem :: JORDAN:17

for r being real number
for p1, p2 being Point of (TOP-REAL 2) st p1 `2 <= r & r <= p2 `2 holds
LSeg p1,p2 meets Horizontal_Line r

proof end;

Lm4: now

let n be Nat; :: thesis:
let A be Subset of (TOP-REAL n); :: thesis:
assume A1: A is empty ; :: thesis:
consider p being Point of (TOP-REAL n);
A c= {p} by A1, XBOOLE_1:2;
hence A is Bounded by JORDAN2C:16; :: thesis:

end;

registration

let n be Nat;
cluster empty -> Bounded Element of bool the carrier of (TOP-REAL n);
coherence by Lm4;
cluster non Bounded -> non empty Element of bool the carrier of (TOP-REAL n);
coherence by Lm4;

end;

registration

let n be non empty Nat;
cluster non empty open closed non Bounded convex Element of bool the carrier of (TOP-REAL n);
existence

proof end;

end;

theorem Th18: :: JORDAN:18

for C being compact Subset of (TOP-REAL 2) holds (north_halfline (UMP C)) \ {(UMP C)} misses C

proof end;

theorem Th19: :: JORDAN:19

for C being compact Subset of (TOP-REAL 2) holds (south_halfline (LMP C)) \ {(LMP C)} misses C

proof end;

Lm5: for A being non empty convex Subset of (TOP-REAL 2) holds A is connected
;

theorem Th20: :: JORDAN:20

for C being compact Subset of (TOP-REAL 2) holds (north_halfline (UMP C)) \ {(UMP C)} c= UBD C

proof end;

theorem Th21: :: JORDAN:21

for C being compact Subset of (TOP-REAL 2) holds (south_halfline (LMP C)) \ {(LMP C)} c= UBD C

proof end;

theorem Th22: :: JORDAN:22

for A, B being Subset of (TOP-REAL 2) st A is_inside_component_of B holds
UBD B misses A

proof end;

theorem :: JORDAN:23

for A, B being Subset of (TOP-REAL 2) st A is_outside_component_of B holds
BDD B misses A

proof end;

Lm6: for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve
for U being Subset of ((TOP-REAL 2) | (C ` )) st p in C holds
{p} misses U

proof end;

set C0 = Closed-Interval-TSpace 0,1;

set C1 = Closed-Interval-TSpace (- 1),1;

set l0 = (#) (- 1),1;

set l1 = (- 1),1 (#) ;

set h1 = L[01] ((#) (- 1),1),((- 1),1 (#) );

Lm7: the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] = [:the carrier of (TOP-REAL 2),the carrier of (TOP-REAL 2):]
by BORSUK_1:def 5;

Lm8: [#] (TOP-REAL 2) = the carrier of (TOP-REAL 2)
by PRE_TOPC:12;

Lm9: now

let T be non empty TopSpace; :: thesis:
let a be Real; :: thesis:
set c = the carrier of T;
set f = the carrier of T --> a;
thus the carrier of T --> a is continuous :: thesis:

proof

A1: dom (the carrier of T --> a) = the carrier of T by FUNCT_2:def 1;
A2: rng (the carrier of T --> a) = {a} by FUNCOP_1:14;
let Y be Subset of REAL ; :: according to PSCOMP_1:def 25 :: thesis:
assume Y is closed ; :: thesis:

per cases ;

suppose a in Y ; :: thesis:

then A3: rng (the carrier of T --> a) c= Y by A2, ZFMISC_1:37;
(the carrier of T --> a) " Y = (the carrier of T --> a) " ((rng (the carrier of T --> a)) /\ Y) by RELAT_1:168
.= (the carrier of T --> a) " (rng (the carrier of T --> a)) by A3, XBOOLE_1:28
.= the carrier of T by A1, RELAT_1:169
.= [#] T by PRE_TOPC:12 ;
hence (the carrier of T --> a) " Y is closed ; :: thesis:

end;

suppose not a in Y ; :: thesis:

then A4: rng (the carrier of T --> a) misses Y by A2, ZFMISC_1:56;
(the carrier of T --> a) " Y = (the carrier of T --> a) " ((rng (the carrier of T --> a)) /\ Y) by RELAT_1:168
.= (the carrier of T --> a) " {} by A4, XBOOLE_0:def 7
.= {} T by RELAT_1:171 ;
hence (the carrier of T --> a) " Y is closed ; :: thesis:

end;

theorem Th24: :: JORDAN:24

for n being Nat
for r being real positive number
for a being Point of (TOP-REAL n) holds a in Ball a,r

proof end;

theorem Th25: :: JORDAN:25

for n being Nat
for r being real non negative number
for p being Point of (TOP-REAL n) holds p is Point of (Tdisk p,r)

proof end;

registration

let r be real positive number ;
let n be non empty Nat;
let p, q be Point of (TOP-REAL n);
cluster (cl_Ball p,r) \ {q} -> non empty ;
coherence

proof end;

end;

theorem Th26: :: JORDAN:26

for r, s being real number
for n being Nat
for x being Point of (TOP-REAL n) st r <= s holds
Ball x,r c= Ball x,s

proof end;

theorem Th27: :: JORDAN:27

for r being real number
for n being Nat
for x being Point of (TOP-REAL n) holds (cl_Ball x,r) \ (Ball x,r) = Sphere x,r

proof end;

theorem Th28: :: JORDAN:28

for r being real number
for n being Nat
for y, x being Point of (TOP-REAL n) st y in Sphere x,r holds
(LSeg x,y) \ {x,y} c= Ball x,r

proof end;

theorem Th29: :: JORDAN:29

for r, s being real number
for n being Nat
for x being Point of (TOP-REAL n) st r < s holds
cl_Ball x,r c= Ball x,s

proof end;

theorem Th30: :: JORDAN:30

for r, s being real number
for n being Nat
for x being Point of (TOP-REAL n) st r < s holds
Sphere x,r c= Ball x,s

proof end;

theorem Th31: :: JORDAN:31

for n being Nat
for x being Point of (TOP-REAL n)
for r being non zero real number holds Cl (Ball x,r) = cl_Ball x,r

proof end;

theorem Th32: :: JORDAN:32

for n being Nat
for x being Point of (TOP-REAL n)
for r being non zero real number holds Fr (Ball x,r) = Sphere x,r

proof end;

registration

let n be non empty Nat;
cluster Bounded -> proper Element of bool the carrier of (TOP-REAL n);
coherence

proof end;

end;

registration

let n be Nat;
cluster non empty closed Bounded convex Element of bool the carrier of (TOP-REAL n);
existence

proof end;

cluster non empty open Bounded convex Element of bool the carrier of (TOP-REAL n);
existence

proof end;

end;

registration

let n be Nat;
let A be Bounded Subset of (TOP-REAL n);
cluster Cl A -> Bounded ;
coherence by TOPREAL6:71;

end;

registration

let n be Nat;
let A be Bounded Subset of (TOP-REAL n);
cluster Fr A -> Bounded ;
coherence by JORDAN1I:1;

end;

theorem Th33: :: JORDAN:33

for n being Nat
for A being closed Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st not p in A holds
ex r being real positive number st Ball p,r misses A

proof end;

theorem Th34: :: JORDAN:34

for n being Nat
for A being Bounded Subset of (TOP-REAL n)
for a being Point of (TOP-REAL n) ex r being real positive number st A c= Ball a,r

proof end;

theorem Th35: :: JORDAN:35

for S, T being TopStruct
for f being Function of S,T st f is_homeomorphism holds
f is onto

proof end;

theorem Th36: :: JORDAN:36

for T being TopSpace
for S being SubSpace of T
for A being Subset of T
for B being Subset of S st A = B holds
T | A = S | B

proof end;

registration

let T be non empty being_T2 TopSpace;
cluster non empty -> non empty being_T2 SubSpace of T;
coherence by TOPMETR:3;

end;

registration

let p be Point of (TOP-REAL 2);
let r be real number ;
cluster Tdisk p,r -> closed ;
coherence

proof end;

end;

registration

let p be Point of (TOP-REAL 2);
let r be real number ;
cluster Tdisk p,r -> compact closed ;
coherence

proof end;

end;

theorem :: JORDAN:37

for T being non empty TopSpace
for a, b being Point of T
for f being Path of a,b st a,b are_connected holds
rng f is connected

proof end;

theorem Th38: :: JORDAN:38

for X being non empty TopSpace
for Y being non empty SubSpace of X
for x1, x2 being Point of X
for y1, y2 being Point of Y
for f being Path of x1,x2 st x1 = y1 & x2 = y2 & x1,x2 are_connected & rng f c= the carrier of Y holds
( y1,y2 are_connected & f is Path of y1,y2 )

proof end;

theorem Th39: :: JORDAN:39

for X being non empty arcwise_connected TopSpace
for Y being non empty SubSpace of X
for x1, x2 being Point of X
for y1, y2 being Point of Y
for f being Path of x1,x2 st x1 = y1 & x2 = y2 & rng f c= the carrier of Y holds
( y1,y2 are_connected & f is Path of y1,y2 )

proof end;

Lm10: for T being non empty TopSpace
for a, b being Point of T
for f being Path of a,b st a,b are_connected holds
rng f c= rng (- f)

proof end;

theorem Th40: :: JORDAN:40

for T being non empty TopSpace
for a, b being Point of T
for f being Path of a,b st a,b are_connected holds
rng f = rng (- f)

proof end;

theorem Th41: :: JORDAN:41

for T being non empty arcwise_connected TopSpace
for a, b being Point of T
for f being Path of a,b holds rng f = rng (- f)

proof end;

theorem Th42: :: JORDAN:42

for T being non empty TopSpace
for a, b, c being Point of T
for f being Path of a,b
for g being Path of b,c st a,b are_connected & b,c are_connected holds
rng f c= rng (f + g)

proof end;

theorem :: JORDAN:43

for T being non empty arcwise_connected TopSpace
for a, b, c being Point of T
for f being Path of a,b
for g being Path of b,c holds rng f c= rng (f + g)

proof end;

theorem Th44: :: JORDAN:44

for T being non empty TopSpace
for a, b, c being Point of T
for f being Path of b,c
for g being Path of a,b st a,b are_connected & b,c are_connected holds
rng f c= rng (g + f)

proof end;

theorem :: JORDAN:45

for T being non empty arcwise_connected TopSpace
for a, b, c being Point of T
for f being Path of b,c
for g being Path of a,b holds rng f c= rng (g + f)

proof end;

theorem Th46: :: JORDAN:46

for T being non empty TopSpace
for a, b, c being Point of T
for f being Path of a,b
for g being Path of b,c st a,b are_connected & b,c are_connected holds
rng (f + g) = (rng f) \/ (rng g)

proof end;

theorem :: JORDAN:47

for T being non empty arcwise_connected TopSpace
for a, b, c being Point of T
for f being Path of a,b
for g being Path of b,c holds rng (f + g) = (rng f) \/ (rng g)

proof end;

theorem Th48: :: JORDAN:48

for T being non empty TopSpace
for a, b, c, d being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds
rng ((f + g) + h) = ((rng f) \/ (rng g)) \/ (rng h)

proof end;

theorem Th49: :: JORDAN:49

for T being non empty arcwise_connected TopSpace
for a, b, c, d being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d holds rng ((f + g) + h) = ((rng f) \/ (rng g)) \/ (rng h)

proof end;

Lm11: for T being non empty TopSpace
for a, b, c, d, e being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d
for i being Path of d,e st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds
rng (((f + g) + h) + i) = (((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)

proof end;

Lm12: for T being non empty arcwise_connected TopSpace
for a, b, c, d, e being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d
for i being Path of d,e holds rng (((f + g) + h) + i) = (((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)

proof end;

Lm13: for T being non empty TopSpace
for a, b, c, d, e, z being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d
for i being Path of d,e
for j being Path of e,z st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & e,z are_connected holds
rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)

proof end;

Lm14: for T being non empty arcwise_connected TopSpace
for a, b, c, d, e, z being Point of T
for f being Path of a,b
for g being Path of b,c
for h being Path of c,d
for i being Path of d,e
for j being Path of e,z holds rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)

proof end;

theorem Th50: :: JORDAN:50

for T being non empty TopSpace
for a being Point of T holds I[01] --> a is Path of a,a

proof end;

theorem Th51: :: JORDAN:51

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
ex F being Path of p1,p2 ex f being Function of I[01] ,((TOP-REAL n) | P) st
( rng f = P & F = f )

proof end;

theorem Th52: :: JORDAN:52

for n being Nat
for p1, p2 being Point of (TOP-REAL n) ex F being Path of p1,p2 ex f being Function of I[01] ,((TOP-REAL n) | (LSeg p1,p2)) st
( rng f = LSeg p1,p2 & F = f )

proof end;

theorem Th53: :: JORDAN:53

for P being Subset of (TOP-REAL 2)
for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 holds
ex f being Path of q1,q2 st
( rng f c= P & rng f misses {p1,p2} )

proof end;

theorem Th54: :: JORDAN:54

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

proof end;

theorem Th55: :: JORDAN:55

for a, b, c, d being real number holds inside_of_rectangle a,b,c,d c= closed_inside_of_rectangle a,b,c,d

proof end;

theorem Th56: :: JORDAN:56

for a, b, c, d being real number holds closed_inside_of_rectangle a,b,c,d = (outside_of_rectangle a,b,c,d) `

proof end;

registration

let a, b, c, d be real number ;
cluster closed_inside_of_rectangle a,b,c,d -> closed ;
coherence

proof end;

end;

theorem Th57: :: JORDAN:57

for a, b, c, d being real number holds closed_inside_of_rectangle a,b,c,d misses outside_of_rectangle a,b,c,d

proof end;

theorem Th58: :: JORDAN:58

for a, b, c, d being real number holds (closed_inside_of_rectangle a,b,c,d) /\ (inside_of_rectangle a,b,c,d) = inside_of_rectangle a,b,c,d

proof end;

theorem Th59: :: JORDAN:59

for a, b, c, d being real number st a < b & c < d holds
Int (closed_inside_of_rectangle a,b,c,d) = inside_of_rectangle a,b,c,d

proof end;

theorem Th60: :: JORDAN:60

for a, b, c, d being real number st a <= b & c <= d holds
(closed_inside_of_rectangle a,b,c,d) \ (inside_of_rectangle a,b,c,d) = rectangle a,b,c,d

proof end;

theorem Th61: :: JORDAN:61

for a, b, c, d being real number st a < b & c < d holds
Fr (closed_inside_of_rectangle a,b,c,d) = rectangle a,b,c,d

proof end;

theorem :: JORDAN:62

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

proof end;

theorem :: JORDAN:63

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

proof end;

theorem :: JORDAN:64

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

proof end;

theorem :: JORDAN:65

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

proof end;

theorem Th66: :: JORDAN:66

for a, b, c, d being real number
for p1, p2 being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st a < b & c < d & p1 in closed_inside_of_rectangle a,b,c,d & not p2 in closed_inside_of_rectangle a,b,c,d & P is_an_arc_of p1,p2 holds
Segment P,p1,p2,p1,(First_Point P,p1,p2,(rectangle a,b,c,d)) c= closed_inside_of_rectangle a,b,c,d

proof end;

definition

let S, T be non empty TopSpace;
let x be Point of [:S,T:];
:: original: `1
redefine func x `1 -> Element of S;
coherence

proof end;

:: original: `2
redefine func x `2 -> Element of T;
coherence

proof end;

end;

definition

let o be Point of (TOP-REAL 2);
func diffX2_1 o -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def1: :: JORDAN:def 1
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = ((x `2 ) `1 ) - (o `1 );
existence

proof end;

uniqueness

proof end;

func diffX2_2 o -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def2: :: JORDAN:def 2
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = ((x `2 ) `2 ) - (o `2 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines diffX2_1 JORDAN:def 1 :

:: deftheorem Def2 defines diffX2_2 JORDAN:def 2 :

definition

func diffX1_X2_1 -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def3: :: JORDAN:def 3
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = ((x `1 ) `1 ) - ((x `2 ) `1 );
existence

proof end;

uniqueness

proof end;

func diffX1_X2_2 -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def4: :: JORDAN:def 4
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = ((x `1 ) `2 ) - ((x `2 ) `2 );
existence

proof end;

uniqueness

proof end;

func Proj2_1 -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def5: :: JORDAN:def 5
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = (x `2 ) `1 ;
existence

proof end;

uniqueness

proof end;

func Proj2_2 -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def6: :: JORDAN:def 6
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = (x `2 ) `2 ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines diffX1_X2_1 JORDAN:def 3 :

:: deftheorem Def4 defines diffX1_X2_2 JORDAN:def 4 :

:: deftheorem Def5 defines Proj2_1 JORDAN:def 5 :

:: deftheorem Def6 defines Proj2_2 JORDAN:def 6 :

theorem Th67: :: JORDAN:67

for o being Point of (TOP-REAL 2) holds diffX2_1 o is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1

proof end;

theorem Th68: :: JORDAN:68

for o being Point of (TOP-REAL 2) holds diffX2_2 o is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1

proof end;

theorem Th69: :: JORDAN:69

diffX1_X2_1 is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1

proof end;

theorem Th70: :: JORDAN:70

diffX1_X2_2 is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1

proof end;

theorem Th71: :: JORDAN:71

Proj2_1 is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1

proof end;

theorem Th72: :: JORDAN:72

Proj2_2 is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1

proof end;

registration

let o be Point of (TOP-REAL 2);
cluster diffX2_1 o -> continuous ;
coherence

proof end;

cluster diffX2_2 o -> continuous ;
coherence

proof end;

end;

registration

cluster diffX1_X2_1 -> continuous ;
coherence by Th69, TOPREAL6:83;
cluster diffX1_X2_2 -> continuous ;
coherence by Th70, TOPREAL6:83;
cluster Proj2_1 -> continuous ;
coherence by Th71, TOPREAL6:83;
cluster Proj2_2 -> continuous ;
coherence by Th72, TOPREAL6:83;

end;

definition

let n be non empty Nat;
let o, p be Point of (TOP-REAL n);
let r be real positive number ;
assume A1: p is Point of (Tdisk o,r) ;
set X = (TOP-REAL n) | ((cl_Ball o,r) \ {p});
func DiskProj o,r,p -> Function of ((TOP-REAL n) | ((cl_Ball o,r) \ {p})),(Tcircle o,r) means :Def7: :: JORDAN:def 7
for x being Point of ((TOP-REAL n) | ((cl_Ball o,r) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y & it . x = HC p,y,o,r );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines DiskProj JORDAN:def 7 :

theorem Th73: :: JORDAN:73

for o, p being Point of (TOP-REAL 2)
for r being real positive number st p is Point of (Tdisk o,r) holds
DiskProj o,r,p is continuous

proof end;

theorem Th74: :: JORDAN:74

for n being non empty Nat
for o, p being Point of (TOP-REAL n)
for r being real positive number st p in Ball o,r holds
(DiskProj o,r,p) | (Sphere o,r) = id (Sphere o,r)

proof end;

definition

let n be non empty Nat;
let o, p be Point of (TOP-REAL n);
let r be real positive number ;
assume A1: p in Ball o,r ;
set X = Tcircle o,r;
func RotateCircle o,r,p -> Function of (Tcircle o,r),(Tcircle o,r) means :Def8: :: JORDAN:def 8
for x being Point of (Tcircle o,r) ex y being Point of (TOP-REAL n) st
( x = y & it . x = HC y,p,o,r );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines RotateCircle JORDAN:def 8 :

theorem Th75: :: JORDAN:75

for o, p being Point of (TOP-REAL 2)
for r being real positive number st p in Ball o,r holds
RotateCircle o,r,p is continuous

proof end;

theorem Th76: :: JORDAN:76

for n being non empty Nat
for o, p being Point of (TOP-REAL n)
for r being real positive number st p in Ball o,r holds
RotateCircle o,r,p has_no_fixpoint

proof end;

theorem Th77: :: JORDAN:77

for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2)
for U, V being Subset of ((TOP-REAL 2) | (C ` )) st U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) & V is_a_component_of (TOP-REAL 2) | (C ` ) & U <> V holds
Cl P misses V

proof end;

theorem Th78: :: JORDAN:78

for C being Simple_closed_curve
for U being Subset of ((TOP-REAL 2) | (C ` )) st U is_a_component_of (TOP-REAL 2) | (C ` ) holds
((TOP-REAL 2) | (C ` )) | U is arcwise_connected

proof end;

Lm15: for p1, p2, p being Point of (TOP-REAL 2)
for A being Subset of (TOP-REAL 2)
for r being real non negative number st A is_an_arc_of p1,p2 & A is Subset of (Tdisk p,r) holds
ex f being Function of (Tdisk p,r),((TOP-REAL 2) | A) st
( f is continuous & f | A = id A )

proof end;

Lm16: for p1, p2, p being Point of (TOP-REAL 2)
for C being Simple_closed_curve
for A, P, B being Subset of (TOP-REAL 2)
for U being Subset of ((TOP-REAL 2) | (C ` ))
for r being real positive number st A is_an_arc_of p1,p2 & A c= C & C c= Ball p,r & p in U & (Cl P) /\ (P ` ) c= A & P c= Ball p,r holds
for f being Function of (Tdisk p,r),((TOP-REAL 2) | A) st f is continuous & f | A = id A & U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) & B = (cl_Ball p,r) \ {p} holds
ex g being Function of (Tdisk p,r),((TOP-REAL 2) | B) st
( g is continuous & ( for x being Point of (Tdisk p,r) holds
( ( x in Cl P implies g . x = f . x ) & ( x in P ` implies g . x = x ) ) ) )

proof end;

Lm17: for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve
for P, B being Subset of (TOP-REAL 2)
for U, V being Subset of ((TOP-REAL 2) | (C ` ))
for A being non empty Subset of (TOP-REAL 2)
for P1 being Subset of (TOP-REAL 2) st U <> V holds
for r being real positive number st A c= C & C c= Ball p,r & p in V & (Cl P) /\ (P ` ) c= A & Ball p,r meets P holds
for f being Function of (Tdisk p,r),((TOP-REAL 2) | A) st f is continuous & f | A = id A & U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) & V is_a_component_of (TOP-REAL 2) | (C ` ) & B = (cl_Ball p,r) \ {p} holds
ex g being Function of (Tdisk p,r),((TOP-REAL 2) | B) st
( g is continuous & ( for x being Point of (Tdisk p,r) holds
( ( x in Cl P implies g . x = x ) & ( x in P ` implies g . x = f . x ) ) ) )

proof end;

theorem Th79: :: JORDAN:79

for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2)
for U being Subset of ((TOP-REAL 2) | (C ` )) st U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) holds
C = Fr P

proof end;

set rp = 1;

set rl = - 1;

set rg = 3;

set rd = - 3;

set a = |[(- 1),0]|;

set b = |[1,0]|;

set c = |[0,3]|;

set d = |[0,(- 3)]|;

set lg = |[(- 1),3]|;

set pg = |[1,3]|;

set ld = |[(- 1),(- 3)]|;

set pd = |[1,(- 3)]|;

set R = closed_inside_of_rectangle (- 1),1,(- 3),3;

set dR = rectangle (- 1),1,(- 3),3;

set TR = Trectangle (- 1),1,(- 3),3;

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

Lm19: |[1,0]| `1 = 1
by EUCLID:56;

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

Lm21: |[1,0]| `2 = 0
by EUCLID:56;

Lm22: |[0,3]| `1 = 0
by EUCLID:56;

Lm23: |[0,3]| `2 = 3
by EUCLID:56;

Lm24: |[0,(- 3)]| `1 = 0
by EUCLID:56;

Lm25: |[0,(- 3)]| `2 = - 3
by EUCLID:56;

Lm26: |[(- 1),3]| `1 = - 1
by EUCLID:56;

Lm27: |[(- 1),3]| `2 = 3
by EUCLID:56;

Lm28: |[(- 1),(- 3)]| `1 = - 1
by EUCLID:56;

Lm29: |[(- 1),(- 3)]| `2 = - 3
by EUCLID:56;

Lm30: |[1,3]| `1 = 1
by EUCLID:56;

Lm31: |[1,3]| `2 = 3
by EUCLID:56;

Lm32: |[1,(- 3)]| `1 = 1
by EUCLID:56;

Lm33: |[1,(- 3)]| `2 = - 3
by EUCLID:56;

Lm34: |[(- 1),(- 3)]| = |[(|[(- 1),(- 3)]| `1 ),(|[(- 1),(- 3)]| `2 )]|
by EUCLID:57;

Lm35: |[(- 1),3]| = |[(|[(- 1),3]| `1 ),(|[(- 1),3]| `2 )]|
by EUCLID:57;

Lm36: |[1,(- 3)]| = |[(|[1,(- 3)]| `1 ),(|[1,(- 3)]| `2 )]|
by EUCLID:57;

Lm37: |[1,3]| = |[(|[1,3]| `1 ),(|[1,3]| `2 )]|
by EUCLID:57;

Lm38: rectangle (- 1),1,(- 3),3 = ((LSeg |[(- 1),(- 3)]|,|[(- 1),3]|) \/ (LSeg |[(- 1),3]|,|[1,3]|)) \/ ((LSeg |[1,3]|,|[1,(- 3)]|) \/ (LSeg |[1,(- 3)]|,|[(- 1),(- 3)]|))
by SPPOL_2:def 3;

( LSeg |[(- 1),(- 3)]|,|[(- 1),3]| c= (LSeg |[(- 1),(- 3)]|,|[(- 1),3]|) \/ (LSeg |[(- 1),3]|,|[1,3]|) & (LSeg |[(- 1),(- 3)]|,|[(- 1),3]|) \/ (LSeg |[(- 1),3]|,|[1,3]|) c= rectangle (- 1),1,(- 3),3 )
by Lm38, XBOOLE_1:7;

then Lm39: LSeg |[(- 1),(- 3)]|,|[(- 1),3]| c= rectangle (- 1),1,(- 3),3
by XBOOLE_1:1;

( LSeg |[(- 1),3]|,|[1,3]| c= (LSeg |[(- 1),(- 3)]|,|[(- 1),3]|) \/ (LSeg |[(- 1),3]|,|[1,3]|) & (LSeg |[(- 1),(- 3)]|,|[(- 1),3]|) \/ (LSeg |[(- 1),3]|,|[1,3]|) c= rectangle (- 1),1,(- 3),3 )
by Lm38, XBOOLE_1:7;

then Lm40: LSeg |[(- 1),3]|,|[1,3]| c= rectangle (- 1),1,(- 3),3
by XBOOLE_1:1;

( LSeg |[1,3]|,|[1,(- 3)]| c= (LSeg |[1,3]|,|[1,(- 3)]|) \/ (LSeg |[1,(- 3)]|,|[(- 1),(- 3)]|) & (LSeg |[1,3]|,|[1,(- 3)]|) \/ (LSeg |[1,(- 3)]|,|[(- 1),(- 3)]|) c= rectangle (- 1),1,(- 3),3 )
by Lm38, XBOOLE_1:7;

then Lm41: LSeg |[1,3]|,|[1,(- 3)]| c= rectangle (- 1),1,(- 3),3
by XBOOLE_1:1;

( LSeg |[1,(- 3)]|,|[(- 1),(- 3)]| c= (LSeg |[1,3]|,|[1,(- 3)]|) \/ (LSeg |[1,(- 3)]|,|[(- 1),(- 3)]|) & (LSeg |[1,3]|,|[1,(- 3)]|) \/ (LSeg |[1,(- 3)]|,|[(- 1),(- 3)]|) c= rectangle (- 1),1,(- 3),3 )
by Lm38, XBOOLE_1:7;

then Lm42: LSeg |[1,(- 3)]|,|[(- 1),(- 3)]| c= rectangle (- 1),1,(- 3),3
by XBOOLE_1:1;

Lm43: LSeg |[(- 1),(- 3)]|,|[(- 1),3]| is vertical
by Lm26, Lm28, SPPOL_1:37;

Lm44: LSeg |[1,(- 3)]|,|[1,3]| is vertical
by Lm30, Lm32, SPPOL_1:37;

Lm45: LSeg |[(- 1),0]|,|[(- 1),3]| is vertical
by Lm18, Lm26, SPPOL_1:37;

Lm46: LSeg |[(- 1),0]|,|[(- 1),(- 3)]| is vertical
by Lm18, Lm28, SPPOL_1:37;

Lm47: LSeg |[1,0]|,|[1,3]| is vertical
by Lm19, Lm30, SPPOL_1:37;

Lm48: LSeg |[1,0]|,|[1,(- 3)]| is vertical
by Lm19, Lm32, SPPOL_1:37;

Lm49: LSeg |[(- 1),(- 3)]|,|[0,(- 3)]| is horizontal
by Lm29, Lm25, SPPOL_1:36;

Lm50: LSeg |[1,(- 3)]|,|[0,(- 3)]| is horizontal
by Lm33, Lm25, SPPOL_1:36;

Lm51: LSeg |[(- 1),3]|,|[0,3]| is horizontal
by Lm27, Lm23, SPPOL_1:36;

Lm52: LSeg |[1,3]|,|[0,3]| is horizontal
by Lm31, Lm23, SPPOL_1:36;

Lm53: LSeg |[(- 1),3]|,|[1,3]| is horizontal
by Lm27, Lm31, SPPOL_1:36;

Lm54: LSeg |[(- 1),(- 3)]|,|[1,(- 3)]| is horizontal
by Lm29, Lm33, SPPOL_1:36;

Lm55: LSeg |[(- 1),0]|,|[(- 1),3]| c= LSeg |[(- 1),(- 3)]|,|[(- 1),3]|
by Lm43, Lm45, Lm18, Lm28, Lm20, Lm27, Lm29, JORDAN15:5;

Lm56: LSeg |[(- 1),0]|,|[(- 1),(- 3)]| c= LSeg |[(- 1),(- 3)]|,|[(- 1),3]|
by Lm43, Lm46, Lm28, Lm20, Lm27, Lm29, JORDAN15:5;

Lm57: LSeg |[1,0]|,|[1,3]| c= LSeg |[1,(- 3)]|,|[1,3]|
by Lm47, Lm44, Lm19, Lm32, Lm31, Lm33, Lm21, JORDAN15:5;

Lm58: LSeg |[1,0]|,|[1,(- 3)]| c= LSeg |[1,(- 3)]|,|[1,3]|
by Lm48, Lm44, Lm32, Lm21, Lm31, Lm33, JORDAN15:5;

Lm59: rectangle (- 1),1,(- 3),3 = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = - 1 & p `2 <= 3 & p `2 >= - 3 ) or ( p `1 <= 1 & p `1 >= - 1 & p `2 = 3 ) or ( p `1 <= 1 & p `1 >= - 1 & p `2 = - 3 ) or ( p `1 = 1 & p `2 <= 3 & p `2 >= - 3 ) ) }
by SPPOL_2:58;

then Lm60: |[0,3]| in rectangle (- 1),1,(- 3),3
by Lm22, Lm23;

Lm61: |[0,(- 3)]| in rectangle (- 1),1,(- 3),3
by Lm24, Lm25, Lm59;

Lm62: (2 + 1) ^2 = (4 + 4) + 1
;

then Lm63: sqrt 9 = 3
by SQUARE_1:def 4;

Lm64: dist |[(- 1),0]|,|[1,0]| = sqrt ((((|[(- 1),0]| `1 ) - (|[1,0]| `1 )) ^2 ) + (((|[(- 1),0]| `2 ) - (|[1,0]| `2 )) ^2 )) by GOBRD14:9
.= - (- 2) by Lm18, Lm19, Lm20, Lm21, SQUARE_1:90 ;

theorem Th80: :: JORDAN:80

for C being Simple_closed_curve
for h being Homeomorphism of TOP-REAL 2 holds h .: C is being_simple_closed_curve

proof end;

theorem Th81: :: JORDAN:81

for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
P c= closed_inside_of_rectangle (- 1),1,(- 3),3

proof end;

Lm65: rectangle (- 1),1,(- 3),3 c= closed_inside_of_rectangle (- 1),1,(- 3),3
by Th54;

( |[(- 1),3]| `2 = |[(- 1),3]| `2 & |[(- 1),3]| `1 <= |[0,3]| `1 & |[0,3]| `1 <= |[1,3]| `1 )
by Lm26, Lm30, EUCLID:56;

then LSeg |[(- 1),3]|,|[0,3]| c= LSeg |[(- 1),3]|,|[1,3]|
by Lm51, Lm53, JORDAN15:6;

then Lm66: LSeg |[(- 1),3]|,|[0,3]| c= rectangle (- 1),1,(- 3),3
by Lm40, XBOOLE_1:1;

LSeg |[1,3]|,|[0,3]| c= LSeg |[(- 1),3]|,|[1,3]|
by Lm52, Lm53, Lm22, Lm23, Lm26, Lm27, Lm30, JORDAN15:6;

then Lm67: LSeg |[1,3]|,|[0,3]| c= rectangle (- 1),1,(- 3),3
by Lm40, XBOOLE_1:1;

( |[(- 1),(- 3)]| `2 = |[(- 1),(- 3)]| `2 & |[(- 1),(- 3)]| `1 <= |[0,(- 3)]| `1 & |[0,(- 3)]| `1 <= |[1,(- 3)]| `1 )
by Lm28, Lm32, EUCLID:56;

then LSeg |[(- 1),(- 3)]|,|[0,(- 3)]| c= LSeg |[(- 1),(- 3)]|,|[1,(- 3)]|
by Lm49, Lm54, JORDAN15:6;

then Lm68: LSeg |[(- 1),(- 3)]|,|[0,(- 3)]| c= rectangle (- 1),1,(- 3),3
by Lm42, XBOOLE_1:1;

LSeg |[1,(- 3)]|,|[0,(- 3)]| c= LSeg |[(- 1),(- 3)]|,|[1,(- 3)]|
by Lm50, Lm54, Lm24, Lm25, Lm28, Lm29, Lm32, JORDAN15:6;

then Lm69: LSeg |[1,(- 3)]|,|[0,(- 3)]| c= rectangle (- 1),1,(- 3),3
by Lm42, XBOOLE_1:1;

Lm70: for p being Point of (TOP-REAL 2) st 0 <= p `2 & p in rectangle (- 1),1,(- 3),3 & not p in LSeg |[(- 1),0]|,|[(- 1),3]| & not p in LSeg |[(- 1),3]|,|[0,3]| & not p in LSeg |[0,3]|,|[1,3]| holds
p in LSeg |[1,3]|,|[1,0]|

proof end;

Lm71: for p being Point of (TOP-REAL 2) st p `2 <= 0 & p in rectangle (- 1),1,(- 3),3 & not p in LSeg |[(- 1),0]|,|[(- 1),(- 3)]| & not p in LSeg |[(- 1),(- 3)]|,|[0,(- 3)]| & not p in LSeg |[0,(- 3)]|,|[1,(- 3)]| holds
p in LSeg |[1,(- 3)]|,|[1,0]|

proof end;

theorem Th82: :: JORDAN:82

for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
P misses LSeg |[(- 1),3]|,|[1,3]|

proof end;

theorem Th83: :: JORDAN:83

for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
P misses LSeg |[(- 1),(- 3)]|,|[1,(- 3)]|

proof end;

theorem Th84: :: JORDAN:84

for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
P /\ (rectangle (- 1),1,(- 3),3) = {|[(- 1),0]|,|[1,0]|}

proof end;

Lm72: for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
LSeg |[(- 1),3]|,|[0,3]| misses C

proof end;

Lm73: for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
LSeg |[1,3]|,|[0,3]| misses C

proof end;

Lm74: for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
LSeg |[(- 1),(- 3)]|,|[0,(- 3)]| misses C

proof end;

Lm75: for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
LSeg |[1,(- 3)]|,|[0,(- 3)]| misses C

proof end;

Lm76: for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C & p in C ` & p in LSeg |[(- 1),0]|,|[(- 1),3]| holds
LSeg p,|[(- 1),3]| misses C

proof end;

Lm77: for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C & p in C ` & p in LSeg |[1,0]|,|[1,3]| holds
LSeg p,|[1,3]| misses C

proof end;

Lm78: for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C & p in C ` & p in LSeg |[(- 1),0]|,|[(- 1),(- 3)]| holds
LSeg p,|[(- 1),(- 3)]| misses C

proof end;

Lm79: for p being Point of (TOP-REAL 2)
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C & p in C ` & p in LSeg |[1,0]|,|[1,(- 3)]| holds
LSeg p,|[1,(- 3)]| misses C

proof end;

Lm80: for r being real number holds
( not |[0,r]| in rectangle (- 1),1,(- 3),3 or r = - 3 or r = 3 )

proof end;

theorem Th85: :: JORDAN:85

for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
W-bound P = - 1

proof end;

theorem Th86: :: JORDAN:86

for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
E-bound P = 1

proof end;

theorem Th87: :: JORDAN:87

for P being compact Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
W-most P = {|[(- 1),0]|}

proof end;

theorem Th88: :: JORDAN:88

for P being compact Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
E-most P = {|[1,0]|}

proof end;

theorem Th89: :: JORDAN:89

for P being compact Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
( W-min P = |[(- 1),0]| & W-max P = |[(- 1),0]| )

proof end;

theorem Th90: :: JORDAN:90

for P being compact Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
( E-min P = |[1,0]| & E-max P = |[1,0]| )

proof end;

Lm81: for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
|[0,3]| `1 = ((W-bound P) + (E-bound P)) / 2

proof end;

Lm82: for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
|[0,(- 3)]| `1 = ((W-bound P) + (E-bound P)) / 2

proof end;

theorem Th91: :: JORDAN:91

for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
LSeg |[0,3]|,(UMP P) is vertical

proof end;

theorem Th92: :: JORDAN:92

for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
LSeg (LMP P),|[0,(- 3)]| is vertical

proof end;

theorem Th93: :: JORDAN:93

for p being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P & p in P holds
p `2 < 3

proof end;

theorem Th94: :: JORDAN:94

for p being Point of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P & p in P holds
- 3 < p `2

proof end;

theorem Th95: :: JORDAN:95

for p being Point of (TOP-REAL 2)
for D being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in D & p in LSeg |[0,3]|,(UMP D) holds
(UMP D) `2 <= p `2

proof end;

theorem Th96: :: JORDAN:96

for p being Point of (TOP-REAL 2)
for D being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in D & p in LSeg (LMP D),|[0,(- 3)]| holds
p `2 <= (LMP D) `2

proof end;

theorem Th97: :: JORDAN:97

for D being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in D holds
LSeg |[0,3]|,(UMP D) c= north_halfline (UMP D)

proof end;

theorem Th98: :: JORDAN:98

for D being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in D holds
LSeg (LMP D),|[0,(- 3)]| c= south_halfline (LMP D)

proof end;

theorem Th99: :: JORDAN:99

for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in C & P is_inside_component_of C holds
LSeg |[0,3]|,(UMP C) misses P

proof end;

theorem Th100: :: JORDAN:100

for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in C & P is_inside_component_of C holds
LSeg (LMP C),|[0,(- 3)]| misses P

proof end;

theorem Th101: :: JORDAN:101

for D being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in D holds
(LSeg |[0,3]|,(UMP D)) /\ D = {(UMP D)}

proof end;

theorem :: JORDAN:102

for D being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in D holds
(LSeg |[0,(- 3)]|,(LMP D)) /\ D = {(LMP D)}

proof end;

theorem Th103: :: JORDAN:103

for P, A being Subset of (TOP-REAL 2) st P is compact & |[(- 1),0]|,|[1,0]| realize-max-dist-in P & A is_inside_component_of P holds
A c= closed_inside_of_rectangle (- 1),1,(- 3),3

proof end;

Lm83: for p being Point of (TOP-REAL 2) st p in closed_inside_of_rectangle (- 1),1,(- 3),3 holds
closed_inside_of_rectangle (- 1),1,(- 3),3 c= Ball p,10

proof end;

theorem :: JORDAN:104

for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
LSeg |[0,3]|,|[0,(- 3)]| meets C

proof end;

Lm84: for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
ex Jc, Jd being compact with_the_max_arc Subset of (TOP-REAL 2) st
( Jc is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc )

proof end;

theorem Th105: :: JORDAN:105

for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
for Jc, Jd being compact with_the_max_arc Subset of (TOP-REAL 2) st Jc is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc holds
for Ux being Subset of (TOP-REAL 2) st Ux = skl (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` )) holds
( Ux is_inside_component_of C & ( for V being Subset of (TOP-REAL 2) st V is_inside_component_of C holds
V = Ux ) )

proof end;

theorem Th106: :: JORDAN:106

for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
for Jc, Jd being compact with_the_max_arc Subset of (TOP-REAL 2) st Jc is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc holds
BDD C = skl (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` ))

proof end;

Lm85: for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
C is Jordan

proof end;

Lm86: for C being Simple_closed_curve holds C is Jordan

proof end;

theorem :: JORDAN:107

for C being Simple_closed_curve ex A1, A2 being Subset of (TOP-REAL 2) st
( C ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (C ` )) st C1 = A1 & C2 = A2 holds
( C1 is_a_component_of (TOP-REAL 2) | (C ` ) & C2 is_a_component_of (TOP-REAL 2) | (C ` ) ) ) )

proof end;

theorem :: JORDAN:108

for C being Simple_closed_curve holds C is Jordan by Lm86;