:: Jordan's Curve Theorem
:: by Artur Korni{\l}owicz
::
:: Received September 15, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

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

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

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

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

registration
let n be Element of NAT ;
let x, y be Point of (TOP-REAL n);
cluster dist (x,y) ->  non negative ;
coherence
 not dist (x,y) is negative
proofend;
end;

theorem Th1: :: JORDAN:1
for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds
(1 / 2) * (p1 + p2) <> p1
proofend;

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

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

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

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

theorem :: JORDAN:6
for p, p1, p2 being Point of (TOP-REAL 2) st p in LSeg (p1,p2) &amp; LSeg (p1,p2) is vertical holds
LSeg (p,p2) is vertical
proofend;

theorem :: JORDAN:7
for p, p1, p2 being Point of (TOP-REAL 2) st p in LSeg (p1,p2) &amp; LSeg (p1,p2) is horizontal holds
LSeg (p,p2) is horizontal
proofend;

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

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

registration
cluster non empty compact vertical  ->  with_the_max_arc for Element of bool the carrier of (TOP-REAL 2);
coherence
 for b1 being Subset of (TOP-REAL 2) st b1 is vertical &amp; not b1 is empty &amp; b1 is compact holds
b1 is with_the_max_arc
proofend;
end;

theorem Th8: :: JORDAN:8
for r being real number
for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <= r &amp; r <= p2 `1 holds
LSeg (p1,p2) meets Vertical_Line r
proofend;

theorem :: JORDAN:9
for r being real number
for p1, p2 being Point of (TOP-REAL 2) st p1 `2 <= r &amp; r <= p2 `2 holds
LSeg (p1,p2) meets Horizontal_Line r
proofend;

registration
let n be Element of NAT ;
cluster empty  ->  bounded for Element of bool the carrier of (TOP-REAL n);
coherence
 for b1 being Subset of (TOP-REAL n) st b1 is empty holds
b1 is bounded ;
cluster non bounded  ->  non empty for Element of bool the carrier of (TOP-REAL n);
coherence
 for b1 being Subset of (TOP-REAL n) st not b1 is bounded holds
not b1 is empty ;
end;

registration
let n be non empty Nat;
cluster functional open closed non bounded convex for Element of bool the carrier of (TOP-REAL n);
existence
 ex b1 being Subset of (TOP-REAL n) st
( b1 is open &amp; b1 is closed &amp; not b1 is bounded &amp; b1 is convex )
proofend;
end;

theorem Th10: :: JORDAN:10
for C being compact Subset of (TOP-REAL 2) holds (north_halfline (UMP C)) \ {(UMP C)} misses C
proofend;

theorem Th11: :: JORDAN:11
for C being compact Subset of (TOP-REAL 2) holds (south_halfline (LMP C)) \ {(LMP C)} misses C
proofend;

theorem Th12: :: JORDAN:12
for C being compact Subset of (TOP-REAL 2) holds (north_halfline (UMP C)) \ {(UMP C)} c= UBD C
proofend;

theorem Th13: :: JORDAN:13
for C being compact Subset of (TOP-REAL 2) holds (south_halfline (LMP C)) \ {(LMP C)} c= UBD C
proofend;

theorem Th14: :: JORDAN:14
for A, B being Subset of (TOP-REAL 2) st A is_inside_component_of B holds
UBD B misses A
proofend;

theorem :: JORDAN:15
for A, B being Subset of (TOP-REAL 2) st A is_outside_component_of B holds
BDD B misses A
proofend;

Lm4:  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
proofend;

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) (#)));

Lm5:  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_2;

Lm6: now__::_thesis:_for_T_being_non_empty_TopSpace
for_a_being_Real_holds_the_carrier_of_T_-->_a_is_continuous
let T be non empty TopSpace; ::_thesis: for a being Real holds the carrier of T --> a is continuous
let a be Real; ::_thesis: the carrier of T --> a is continuous
set c = the carrier of T;
set f = the carrier of T --> a;
thus  the carrier of T --> a is continuous ::_thesis: verum
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:8;
let Y be Subset of REAL; :: according toPSCOMP_1:def_3 ::_thesis: ( not Y is closed or ( the carrier of T --> a) " Y is closed )
assume  Y is closed ; ::_thesis: ( the carrier of T --> a) " Y is closed
percases ( a in Y or not a in Y ) ;
suppose a in Y ; ::_thesis: ( the carrier of T --> a) " Y is closed
then A3: rng ( the carrier of T --> a) c= Y by A2, ZFMISC_1:31;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133
.= ( the carrier of T --> a) " (rng ( the carrier of T --> a)) by A3, XBOOLE_1:28
.= [#] T by A1, RELAT_1:134 ;
hence  ( the carrier of T --> a) " Y is closed ; ::_thesis: verum
end;
suppose not a in Y ; ::_thesis: ( the carrier of T --> a) " Y is closed
then A4: rng ( the carrier of T --> a) misses Y by A2, ZFMISC_1:50;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133
.= ( the carrier of T --> a) " {} by A4, XBOOLE_0:def_7
.= {} T ;
hence  ( the carrier of T --> a) " Y is closed ; ::_thesis: verum
end;
end;
end;
end;

theorem Th16: :: JORDAN:16
for n being Element of NAT
for r being positive real number
for a being Point of (TOP-REAL n) holds a in Ball (a,r)
proofend;

theorem Th17: :: JORDAN:17
for n being Element of NAT
for r being non negative real number
for p being Point of (TOP-REAL n) holds p is Point of (Tdisk (p,r))
proofend;

registration
let r be positive real number ;
let n be non empty Element of NAT ;
let p, q be Point of (TOP-REAL n);
cluster(cl_Ball (p,r)) \ {q} ->  non empty ;
coherence
 not (cl_Ball (p,r)) \ {q} is empty
proofend;
end;

theorem Th18: :: JORDAN:18
for r, s being real number
for n being Element of NAT
for x being Point of (TOP-REAL n) st r <= s holds
Ball (x,r) c= Ball (x,s)
proofend;

theorem Th19: :: JORDAN:19
for r being real number
for n being Element of NAT
for x being Point of (TOP-REAL n) holds (cl_Ball (x,r)) \ (Ball (x,r)) = Sphere (x,r)
proofend;

theorem Th20: :: JORDAN:20
for r being real number
for n being Element of 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)
proofend;

theorem Th21: :: JORDAN:21
for r, s being real number
for n being Element of NAT
for x being Point of (TOP-REAL n) st r < s holds
cl_Ball (x,r) c= Ball (x,s)
proofend;

theorem Th22: :: JORDAN:22
for r, s being real number
for n being Element of NAT
for x being Point of (TOP-REAL n) st r < s holds
Sphere (x,r) c= Ball (x,s)
proofend;

theorem Th23: :: JORDAN:23
for n being Element of 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)
proofend;

theorem Th24: :: JORDAN:24
for n being Element of NAT
for x being Point of (TOP-REAL n)
for r being non zero real number holds Fr (Ball (x,r)) = Sphere (x,r)
proofend;

registration
let n be non empty Element of NAT ;
cluster bounded  ->  proper for Element of bool the carrier of (TOP-REAL n);
coherence
 for b1 being Subset of (TOP-REAL n) st b1 is bounded holds
b1 is proper
proofend;
end;

registration
let n be Element of NAT ;
cluster functional non empty closed bounded convex for Element of bool the carrier of (TOP-REAL n);
existence
 ex b1 being Subset of (TOP-REAL n) st
( not b1 is empty &amp; b1 is closed &amp; b1 is convex &amp; b1 is bounded )
proofend;
cluster functional non empty open bounded convex for Element of bool the carrier of (TOP-REAL n);
existence
 ex b1 being Subset of (TOP-REAL n) st
( not b1 is empty &amp; b1 is open &amp; b1 is convex &amp; b1 is bounded )
proofend;
end;

registration
let n be Element of NAT ;
let A be bounded Subset of (TOP-REAL n);
cluster Cl A ->  bounded ;
coherence
 Cl A is bounded by TOPREAL6:63;
end;

registration
let n be Element of NAT ;
let A be bounded Subset of (TOP-REAL n);
cluster Fr A ->  bounded ;
coherence
 Fr A is bounded by TOPREAL6:89;
end;

theorem Th25: :: JORDAN:25
for n being Element of 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 positive real number st Ball (p,r) misses A
proofend;

theorem Th26: :: JORDAN:26
for n being Element of NAT
for A being bounded Subset of (TOP-REAL n)
for a being Point of (TOP-REAL n) ex r being positive real number st A c= Ball (a,r)
proofend;

theorem :: JORDAN:27
for S, T being TopStruct
for f being Function of S,T st f is being_homeomorphism holds
f is onto ;

registration
let T be non empty T_2 TopSpace;
cluster non empty  ->  non empty T_2 for SubSpace of T;
coherence
 for b1 being non empty SubSpace of T holds b1 is T_2 ;
end;

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

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

begin

theorem :: JORDAN:28
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
proofend;

theorem Th29: :: JORDAN:29
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 &amp; x2 = y2 &amp; x1,x2 are_connected &amp; rng f c= the carrier of Y holds
( y1,y2 are_connected &amp; f is Path of y1,y2 )
proofend;

theorem Th30: :: JORDAN:30
for X being non empty pathwise_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 &amp; x2 = y2 &amp; rng f c= the carrier of Y holds
( y1,y2 are_connected &amp; f is Path of y1,y2 )
proofend;

Lm7:  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)
proofend;

theorem Th31: :: JORDAN:31
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)
proofend;

theorem Th32: :: JORDAN:32
for T being non empty pathwise_connected TopSpace
for a, b being Point of T
for f being Path of a,b holds rng f = rng (- f)
proofend;

theorem Th33: :: JORDAN:33
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 &amp; b,c are_connected holds
rng f c= rng (f + g)
proofend;

theorem :: JORDAN:34
for T being non empty pathwise_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)
proofend;

theorem Th35: :: JORDAN:35
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 &amp; b,c are_connected holds
rng f c= rng (g + f)
proofend;

theorem :: JORDAN:36
for T being non empty pathwise_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)
proofend;

theorem Th37: :: JORDAN:37
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 &amp; b,c are_connected holds
rng (f + g) = (rng f) \/ (rng g)
proofend;

theorem :: JORDAN:38
for T being non empty pathwise_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)
proofend;

theorem Th39: :: JORDAN:39
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 &amp; b,c are_connected &amp; c,d are_connected holds
rng ((f + g) + h) = ((rng f) \/ (rng g)) \/ (rng h)
proofend;

theorem Th40: :: JORDAN:40
for T being non empty pathwise_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)
proofend;

Lm8:  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 &amp; b,c are_connected &amp; c,d are_connected &amp; d,e are_connected holds
rng (((f + g) + h) + i) = (((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)
proofend;

Lm9:  for T being non empty pathwise_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)
proofend;

Lm10:  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 &amp; b,c are_connected &amp; c,d are_connected &amp; d,e are_connected &amp; e,z are_connected holds
rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)
proofend;

Lm11:  for T being non empty pathwise_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)
proofend;

theorem Th41: :: JORDAN:41
for T being non empty TopSpace
for a being Point of T holds I[01] --> a is Path of a,a
proofend;

theorem Th42: :: JORDAN:42
for n being Element of 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 &amp; F = f )
proofend;

theorem Th43: :: JORDAN:43
for n being Element of 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) &amp; F = f )
proofend;

theorem Th44: :: JORDAN:44
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 &amp; q1 in P &amp; q2 in P &amp; q1 <> p1 &amp; q1 <> p2 &amp; q2 <> p1 &amp; q2 <> p2 holds
ex f being Path of q1,q2 st
( rng f c= P &amp; rng f misses {p1,p2} )
proofend;

begin

theorem Th45: :: JORDAN:45
for a, b, c, d being real number st a <= b &amp; c <= d holds
rectangle (a,b,c,d) c= closed_inside_of_rectangle (a,b,c,d)
proofend;

theorem Th46: :: JORDAN:46
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)
proofend;

theorem Th47: :: JORDAN:47
for a, b, c, d being real number holds closed_inside_of_rectangle (a,b,c,d) = (outside_of_rectangle (a,b,c,d)) `
proofend;

registration
let a, b, c, d be real number ;
cluster closed_inside_of_rectangle (a,b,c,d) ->  closed ;
coherence
 closed_inside_of_rectangle (a,b,c,d) is closed
proofend;
end;

theorem Th48: :: JORDAN:48
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)
proofend;

theorem Th49: :: JORDAN:49
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)
proofend;

theorem Th50: :: JORDAN:50
for a, b, c, d being real number st a < b &amp; c < d holds
Int (closed_inside_of_rectangle (a,b,c,d)) = inside_of_rectangle (a,b,c,d)
proofend;

theorem Th51: :: JORDAN:51
for a, b, c, d being real number st a <= b &amp; c <= d holds
(closed_inside_of_rectangle (a,b,c,d)) \ (inside_of_rectangle (a,b,c,d)) = rectangle (a,b,c,d)
proofend;

theorem Th52: :: JORDAN:52
for a, b, c, d being real number st a < b &amp; c < d holds
Fr (closed_inside_of_rectangle (a,b,c,d)) = rectangle (a,b,c,d)
proofend;

theorem :: JORDAN:53
for a, b, c, d being real number st a <= b &amp; c <= d holds
W-bound (closed_inside_of_rectangle (a,b,c,d)) = a
proofend;

theorem :: JORDAN:54
for a, b, c, d being real number st a <= b &amp; c <= d holds
S-bound (closed_inside_of_rectangle (a,b,c,d)) = c
proofend;

theorem :: JORDAN:55
for a, b, c, d being real number st a <= b &amp; c <= d holds
E-bound (closed_inside_of_rectangle (a,b,c,d)) = b
proofend;

theorem :: JORDAN:56
for a, b, c, d being real number st a <= b &amp; c <= d holds
N-bound (closed_inside_of_rectangle (a,b,c,d)) = d
proofend;

theorem Th57: :: JORDAN:57
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 &amp; c < d &amp; p1 in closed_inside_of_rectangle (a,b,c,d) &amp; not p2 in closed_inside_of_rectangle (a,b,c,d) &amp; 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)
proofend;

begin

definition
let S, T be non empty TopSpace;
let x be Point of [:S,T:];
:: original:`1
redefine funcx `1  ->  Element of S;
coherence
 x `1 is Element of S
proofend;
:: original:`2
redefine funcx `2  ->  Element of T;
coherence
 x `2 is Element of T
proofend;
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
 ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `2) `1) - (o `1)
proofend;
uniqueness
 for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `2) `1) - (o `1) ) &amp; ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `2) `1) - (o `1) ) holds
b1 = b2
proofend;
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
 ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `2) `2) - (o `2)
proofend;
uniqueness
 for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `2) `2) - (o `2) ) &amp; ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `2) `2) - (o `2) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines diffX2_1 JORDAN:def_1_:_
 for o being Point of (TOP-REAL 2)
for b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b2 = diffX2_1 o iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `2) `1) - (o `1) );

:: deftheorem Def2 defines diffX2_2 JORDAN:def_2_:_
 for o being Point of (TOP-REAL 2)
for b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b2 = diffX2_2 o iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `2) `2) - (o `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
 ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1) `1) - ((x `2) `1)
proofend;
uniqueness
 for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1) `1) - ((x `2) `1) ) &amp; ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `1) `1) - ((x `2) `1) ) holds
b1 = b2
proofend;
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
 ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1) `2) - ((x `2) `2)
proofend;
uniqueness
 for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1) `2) - ((x `2) `2) ) &amp; ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = ((x `1) `2) - ((x `2) `2) ) holds
b1 = b2
proofend;
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
 ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2) `1
proofend;
uniqueness
 for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2) `1 ) &amp; ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = (x `2) `1 ) holds
b1 = b2
proofend;
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
 ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2) `2
proofend;
uniqueness
 for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2) `2 ) &amp; ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . x = (x `2) `2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines diffX1_X2_1 JORDAN:def_3_:_
 for b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b1 = diffX1_X2_1 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1) `1) - ((x `2) `1) );

:: deftheorem Def4 defines diffX1_X2_2 JORDAN:def_4_:_
 for b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b1 = diffX1_X2_2 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = ((x `1) `2) - ((x `2) `2) );

:: deftheorem Def5 defines Proj2_1 JORDAN:def_5_:_
 for b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b1 = Proj2_1 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2) `1 );

:: deftheorem Def6 defines Proj2_2 JORDAN:def_6_:_
 for b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b1 = Proj2_2 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . x = (x `2) `2 );

theorem Th58: :: JORDAN:58
for o being Point of (TOP-REAL 2) holds diffX2_1 o is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1
proofend;

theorem Th59: :: JORDAN:59
for o being Point of (TOP-REAL 2) holds diffX2_2 o is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1
proofend;

theorem Th60: :: JORDAN:60
diffX1_X2_1 is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1
proofend;

theorem Th61: :: JORDAN:61
diffX1_X2_2 is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1
proofend;

theorem Th62: :: JORDAN:62
Proj2_1 is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1
proofend;

theorem Th63: :: JORDAN:63
Proj2_2 is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1
proofend;

registration
let o be Point of (TOP-REAL 2);
cluster diffX2_1 o ->  continuous ;
coherence
 diffX2_1 o is continuous
proofend;
cluster diffX2_2 o ->  continuous ;
coherence
 diffX2_2 o is continuous
proofend;
end;

registration
cluster diffX1_X2_1  ->  continuous ;
coherence
 diffX1_X2_1 is continuous by Th60, JORDAN5A:27;
cluster diffX1_X2_2  ->  continuous ;
coherence
 diffX1_X2_2 is continuous by Th61, JORDAN5A:27;
cluster Proj2_1  ->  continuous ;
coherence
 Proj2_1 is continuous by Th62, JORDAN5A:27;
cluster Proj2_2  ->  continuous ;
coherence
 Proj2_2 is continuous by Th63, JORDAN5A:27;
end;

definition
let n be non empty Element of NAT ;
let o, p be Point of (TOP-REAL n);
let r be positive real number ;
assume B1: 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 &amp; it . x = HC (p,y,o,r) );
existence
 ex b1 being Function of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})),(Tcircle (o,r)) st
for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y &amp; b1 . x = HC (p,y,o,r) )
proofend;
uniqueness
 for b1, b2 being Function of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})),(Tcircle (o,r)) st ( for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y &amp; b1 . x = HC (p,y,o,r) ) ) &amp; ( for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y &amp; b2 . x = HC (p,y,o,r) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines DiskProj JORDAN:def_7_:_
 for n being non empty Element of NAT
for o, p being Point of (TOP-REAL n)
for r being positive real number st p is Point of (Tdisk (o,r)) holds
for b5 being Function of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})),(Tcircle (o,r)) holds
( b5 = DiskProj (o,r,p) iff for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st
( x = y &amp; b5 . x = HC (p,y,o,r) ) );

theorem Th64: :: JORDAN:64
for o, p being Point of (TOP-REAL 2)
for r being positive real number st p is Point of (Tdisk (o,r)) holds
DiskProj (o,r,p) is continuous
proofend;

theorem Th65: :: JORDAN:65
for n being non empty Element of NAT
for o, p being Point of (TOP-REAL n)
for r being positive real number st p in Ball (o,r) holds
(DiskProj (o,r,p)) | (Sphere (o,r)) = id (Sphere (o,r))
proofend;

definition
let n be non empty Element of NAT ;
let o, p be Point of (TOP-REAL n);
let r be positive real number ;
assume B1: 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 &amp; it . x = HC (y,p,o,r) );
existence
 ex b1 being Function of (Tcircle (o,r)),(Tcircle (o,r)) st
for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y &amp; b1 . x = HC (y,p,o,r) )
proofend;
uniqueness
 for b1, b2 being Function of (Tcircle (o,r)),(Tcircle (o,r)) st ( for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y &amp; b1 . x = HC (y,p,o,r) ) ) &amp; ( for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y &amp; b2 . x = HC (y,p,o,r) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines RotateCircle JORDAN:def_8_:_
 for n being non empty Element of NAT
for o, p being Point of (TOP-REAL n)
for r being positive real number st p in Ball (o,r) holds
for b5 being Function of (Tcircle (o,r)),(Tcircle (o,r)) holds
( b5 = RotateCircle (o,r,p) iff for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st
( x = y &amp; b5 . x = HC (y,p,o,r) ) );

theorem Th66: :: JORDAN:66
for o, p being Point of (TOP-REAL 2)
for r being positive real number st p in Ball (o,r) holds
RotateCircle (o,r,p) is continuous
proofend;

theorem Th67: :: JORDAN:67
for n being non empty Element of NAT
for o, p being Point of (TOP-REAL n)
for r being positive real number st p in Ball (o,r) holds
RotateCircle (o,r,p) is without_fixpoints
proofend;

begin

theorem Th68: :: JORDAN:68
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 &amp; U is a_component &amp; V is a_component &amp; U <> V holds
Cl P misses V
proofend;

theorem Th69: :: JORDAN:69
for C being Simple_closed_curve
for U being Subset of ((TOP-REAL 2) | (C `)) st U is a_component holds
((TOP-REAL 2) | (C `)) | U is pathwise_connected
proofend;

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

Lm13:  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 positive real number st A is_an_arc_of p1,p2 &amp; A c= C &amp; C c= Ball (p,r) &amp; p in U &amp; (Cl P) /\ (P `) c= A &amp; P c= Ball (p,r) holds
for f being Function of (Tdisk (p,r)),((TOP-REAL 2) | A) st f is continuous &amp; f | A = id A &amp; U = P &amp; U is a_component &amp; B = (cl_Ball (p,r)) \ {p} holds
ex g being Function of (Tdisk (p,r)),((TOP-REAL 2) | B) st
( g is continuous &amp; ( for x being Point of (Tdisk (p,r)) holds
( ( x in Cl P implies g . x = f . x ) &amp; ( x in P ` implies g . x = x ) ) ) )
proofend;

Lm14:  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) st U <> V holds
for r being positive real number st A c= C &amp; C c= Ball (p,r) &amp; p in V &amp; (Cl P) /\ (P `) c= A &amp; Ball (p,r) meets P holds
for f being Function of (Tdisk (p,r)),((TOP-REAL 2) | A) st f is continuous &amp; f | A = id A &amp; U = P &amp; U is a_component &amp; V is a_component &amp; B = (cl_Ball (p,r)) \ {p} holds
ex g being Function of (Tdisk (p,r)),((TOP-REAL 2) | B) st
( g is continuous &amp; ( for x being Point of (Tdisk (p,r)) holds
( ( x in Cl P implies g . x = x ) &amp; ( x in P ` implies g . x = f . x ) ) ) )
proofend;

Lm15:  for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2)
for U being Subset of ((TOP-REAL 2) | (C `)) st not BDD C is empty &amp; U = P &amp; U is a_component holds
C = Fr P
proofend;

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

Lm16:  |[(- 1),0]| `1 = - 1
by EUCLID:52;

Lm17:  |[1,0]| `1 = 1
by EUCLID:52;

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

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

Lm20:  |[0,3]| `1 = 0
by EUCLID:52;

Lm21:  |[0,3]| `2 = 3
by EUCLID:52;

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

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

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

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

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

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

Lm28:  |[1,3]| `1 = 1
by EUCLID:52;

Lm29:  |[1,3]| `2 = 3
by EUCLID:52;

Lm30:  |[1,(- 3)]| `1 = 1
by EUCLID:52;

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

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

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

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

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

Lm36:  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;

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

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

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

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

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

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

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

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

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

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

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

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

Lm45:  LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|) is vertical
by Lm24, Lm26, SPPOL_1:16;

Lm46:  LSeg (|[1,(- 3)]|,|[1,3]|) is vertical
by Lm28, Lm30, SPPOL_1:16;

Lm47:  LSeg (|[(- 1),0]|,|[(- 1),3]|) is vertical
by Lm16, Lm24, SPPOL_1:16;

Lm48:  LSeg (|[(- 1),0]|,|[(- 1),(- 3)]|) is vertical
by Lm16, Lm26, SPPOL_1:16;

Lm49:  LSeg (|[1,0]|,|[1,3]|) is vertical
by Lm17, Lm28, SPPOL_1:16;

Lm50:  LSeg (|[1,0]|,|[1,(- 3)]|) is vertical
by Lm17, Lm30, SPPOL_1:16;

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

Lm52:  LSeg (|[1,(- 3)]|,|[0,(- 3)]|) is horizontal
by Lm23, Lm31, SPPOL_1:15;

Lm53:  LSeg (|[(- 1),3]|,|[0,3]|) is horizontal
by Lm21, Lm25, SPPOL_1:15;

Lm54:  LSeg (|[1,3]|,|[0,3]|) is horizontal
by Lm21, Lm29, SPPOL_1:15;

Lm55:  LSeg (|[(- 1),3]|,|[1,3]|) is horizontal
by Lm25, Lm29, SPPOL_1:15;

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

Lm57:  LSeg (|[(- 1),0]|,|[(- 1),3]|) c= LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|)
by Lm16, Lm18, Lm25, Lm26, Lm27, Lm45, Lm47, GOBOARD7:63;

Lm58:  LSeg (|[(- 1),0]|,|[(- 1),(- 3)]|) c= LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|)
by Lm18, Lm25, Lm26, Lm27, Lm45, Lm48, GOBOARD7:63;

Lm59:  LSeg (|[1,0]|,|[1,3]|) c= LSeg (|[1,(- 3)]|,|[1,3]|)
by Lm17, Lm19, Lm29, Lm30, Lm31, Lm46, Lm49, GOBOARD7:63;

Lm60:  LSeg (|[1,0]|,|[1,(- 3)]|) c= LSeg (|[1,(- 3)]|,|[1,3]|)
by Lm19, Lm29, Lm30, Lm31, Lm46, Lm50, GOBOARD7:63;

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

then Lm62:  |[0,3]| in rectangle ((- 1),1,(- 3),3)
by Lm20, Lm21;

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

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

then Lm65:  sqrt 9 = 3
by SQUARE_1:def_2;

Lm66: dist (|[(- 1),0]|,|[1,0]|) = sqrt ((((|[(- 1),0]| `1) - (|[1,0]| `1)) ^2) + (((|[(- 1),0]| `2) - (|[1,0]| `2)) ^2)) by TOPREAL6:92
.= - (- 2) by Lm16, Lm17, Lm18, Lm19, SQUARE_1:23 ;

theorem Th70: :: JORDAN:70
for C being Simple_closed_curve
for h being Homeomorphism of TOP-REAL 2 holds h .: C is being_simple_closed_curve
proofend;

theorem Th71: :: JORDAN:71
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)
proofend;

Lm67:  rectangle ((- 1),1,(- 3),3) c= closed_inside_of_rectangle ((- 1),1,(- 3),3)
by Th45;

Lm68:  |[(- 1),3]| `2 = |[(- 1),3]| `2
;

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

 |[0,3]| `1 <= |[1,3]| `1
by Lm28, EUCLID:52;

then  LSeg (|[(- 1),3]|,|[0,3]|) c= LSeg (|[(- 1),3]|,|[1,3]|)
by Lm53, Lm55, Lm68, Lm69, GOBOARD7:64;

then Lm70:  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 Lm20, Lm21, Lm24, Lm25, Lm28, Lm54, Lm55, GOBOARD7:64;

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

Lm72:  |[(- 1),(- 3)]| `2 = |[(- 1),(- 3)]| `2
;

Lm73:  |[(- 1),(- 3)]| `1 <= |[0,(- 3)]| `1
by Lm26, EUCLID:52;

 |[0,(- 3)]| `1 <= |[1,(- 3)]| `1
by Lm30, EUCLID:52;

then  LSeg (|[(- 1),(- 3)]|,|[0,(- 3)]|) c= LSeg (|[(- 1),(- 3)]|,|[1,(- 3)]|)
by Lm51, Lm56, Lm72, Lm73, GOBOARD7:64;

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

 LSeg (|[1,(- 3)]|,|[0,(- 3)]|) c= LSeg (|[(- 1),(- 3)]|,|[1,(- 3)]|)
by Lm22, Lm23, Lm26, Lm27, Lm30, Lm52, Lm56, GOBOARD7:64;

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

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

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

theorem Th72: :: JORDAN:72
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]|)
proofend;

theorem Th73: :: JORDAN:73
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)]|)
proofend;

theorem Th74: :: JORDAN:74
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]|}
proofend;

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

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

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

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

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

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

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

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

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

theorem Th75: :: JORDAN:75
for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
W-bound P = - 1
proofend;

theorem Th76: :: JORDAN:76
for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in P holds
E-bound P = 1
proofend;

theorem Th77: :: JORDAN:77
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]|}
proofend;

theorem Th78: :: JORDAN:78
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]|}
proofend;

theorem Th79: :: JORDAN:79
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]| &amp; W-max P = |[(- 1),0]| )
proofend;

theorem Th80: :: JORDAN:80
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]| &amp; E-max P = |[1,0]| )
proofend;

Lm87:  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
proofend;

Lm88:  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
proofend;

theorem Th81: :: JORDAN:81
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
proofend;

theorem Th82: :: JORDAN:82
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
proofend;

theorem Th83: :: JORDAN:83
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 &amp; p in P holds
p `2 < 3
proofend;

theorem Th84: :: JORDAN:84
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 &amp; p in P holds
- 3 < p `2
proofend;

theorem Th85: :: JORDAN:85
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 &amp; p in LSeg (|[0,3]|,(UMP D)) holds
(UMP D) `2 <= p `2
proofend;

theorem Th86: :: JORDAN:86
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 &amp; p in LSeg ((LMP D),|[0,(- 3)]|) holds
p `2 <= (LMP D) `2
proofend;

theorem Th87: :: JORDAN:87
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)
proofend;

theorem Th88: :: JORDAN:88
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)
proofend;

theorem Th89: :: JORDAN:89
for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in C &amp; P is_inside_component_of C holds
LSeg (|[0,3]|,(UMP C)) misses P
proofend;

theorem Th90: :: JORDAN:90
for C being Simple_closed_curve
for P being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in C &amp; P is_inside_component_of C holds
LSeg ((LMP C),|[0,(- 3)]|) misses P
proofend;

theorem Th91: :: JORDAN:91
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)}
proofend;

theorem :: JORDAN:92
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)}
proofend;

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

Lm89:  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)
proofend;

theorem :: JORDAN:94
for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C holds
LSeg (|[0,3]|,|[0,(- 3)]|) meets C
proofend;

Lm90:  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]| &amp; Jd is_an_arc_of |[(- 1),0]|,|[1,0]| &amp; C = Jc \/ Jd &amp; Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} &amp; UMP C in Jc &amp; LMP C in Jd &amp; W-bound C = W-bound Jc &amp; E-bound C = E-bound Jc )
proofend;

theorem Th95: :: JORDAN:95
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]| &amp; Jd is_an_arc_of |[(- 1),0]|,|[1,0]| &amp; C = Jc \/ Jd &amp; Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} &amp; UMP C in Jc &amp; LMP C in Jd &amp; W-bound C = W-bound Jc &amp; E-bound C = E-bound Jc holds
for Ux being Subset of (TOP-REAL 2) st Ux = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) holds
( Ux is_inside_component_of C &amp; ( for V being Subset of (TOP-REAL 2) st V is_inside_component_of C holds
V = Ux ) )
proofend;

theorem Th96: :: JORDAN:96
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]| &amp; Jd is_an_arc_of |[(- 1),0]|,|[1,0]| &amp; C = Jc \/ Jd &amp; Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} &amp; UMP C in Jc &amp; LMP C in Jd &amp; W-bound C = W-bound Jc &amp; E-bound C = E-bound Jc holds
BDD C = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `)))
proofend;

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

Lm92:  for C being Simple_closed_curve holds C is Jordan
proofend;

registration
let C be Simple_closed_curve;
cluster BDD C ->  non empty ;
coherence
 not BDD C is empty
proofend;
end;

theorem :: JORDAN:97
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 &amp; U is a_component holds
C = Fr P
proofend;

theorem :: JORDAN:98
for C being Simple_closed_curve ex A1, A2 being Subset of (TOP-REAL 2) st
( C ` = A1 \/ A2 &amp; A1 misses A2 &amp; (Cl A1) \ A1 = (Cl A2) \ A2 &amp; ( for C1, C2 being Subset of ((TOP-REAL 2) | (C `)) st C1 = A1 &amp; C2 = A2 holds
( C1 is a_component &amp; C2 is a_component ) ) )
proofend;

:: [WP: ] Jordan_Curve_Theorem
theorem :: JORDAN:99
for C being Simple_closed_curve holds C is Jordan by Lm92;