:: JORDAN semantic presentation

set c1 = TOP-REAL 2;

Lemma1: for b1, b2, b3, b4 being set st b1 c= b4 & b2 c= b4 & b3 c= b4 holds
(b1 \/ b2) \/ b3 c= b4
proof end;

Lemma2: for b1, b2, b3, b4, b5 being set st b1 c= b5 & b2 c= b5 & b3 c= b5 & b4 c= b5 holds
((b1 \/ b2) \/ b3) \/ b4 c= b5
proof end;

Lemma3: for b1, b2, b3, b4, b5 being set st b1 misses b5 & b2 misses b5 & b3 misses b5 & b4 misses b5 holds
((b1 \/ b2) \/ b3) \/ b4 misses b5
proof end;

registration
let c2 be Reflexive symmetric triangle MetrStruct ;
let c3, c4 be Point of c2;
cluster dist a2,a3 -> non negative ;
coherence
not dist c3,c4 is negative by METRIC_1:5;
end;

registration
let c2 be Nat;
let c3, c4 be Point of (TOP-REAL c2);
cluster dist a2,a3 -> non negative ;
coherence
not dist c3,c4 is negative
proof end;
end;

registration
let c2 be Nat;
let c3, c4 be Point of (TOP-REAL c2);
cluster |.(a2 - a3).| -> non negative ;
coherence
not |.(c3 - c4).| is negative
proof end;
end;

theorem Th1: :: JORDAN:1
for b1 being Nat
for b2, b3 being Point of (TOP-REAL b1) st b2 <> b3 holds
(1 / 2) * (b2 + b3) <> b2
proof end;

theorem Th2: :: JORDAN:2
for b1, b2 being Point of (TOP-REAL 2) st b1 `2 < b2 `2 holds
b1 `2 < ((1 / 2) * (b1 + b2)) `2
proof end;

theorem Th3: :: JORDAN:3
for b1, b2 being Point of (TOP-REAL 2) st b1 `2 < b2 `2 holds
((1 / 2) * (b1 + b2)) `2 < b2 `2
proof end;

theorem Th4: :: JORDAN:4
for b1 being Subset of (TOP-REAL 2)
for b2 being vertical Subset of (TOP-REAL 2) holds b2 /\ b1 is vertical
proof end;

theorem Th5: :: JORDAN:5
for b1 being Subset of (TOP-REAL 2)
for b2 being horizontal Subset of (TOP-REAL 2) holds b2 /\ b1 is horizontal
proof end;

theorem Th6: :: JORDAN:6
for b1, b2, b3 being Point of (TOP-REAL 2) st b1 in LSeg b2,b3 & LSeg b2,b3 is vertical holds
LSeg b1,b3 is vertical
proof end;

theorem Th7: :: JORDAN:7
for b1, b2, b3 being Point of (TOP-REAL 2) st b1 in LSeg b2,b3 & LSeg b2,b3 is horizontal holds
LSeg b1,b3 is horizontal
proof end;

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

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

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

theorem Th8: :: JORDAN:8
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st b1 c= b2 & ( W-min b2 in b1 or W-max b2 in b1 ) holds
W-bound b1 = W-bound b2
proof end;

theorem Th9: :: JORDAN:9
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st b1 c= b2 & ( E-min b2 in b1 or E-max b2 in b1 ) holds
E-bound b1 = E-bound b2
proof end;

theorem Th10: :: JORDAN:10
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st b1 c= b2 & ( N-min b2 in b1 or N-max b2 in b1 ) holds
N-bound b1 = N-bound b2
proof end;

theorem Th11: :: JORDAN:11
for b1, b2 being non empty compact Subset of (TOP-REAL 2) st b1 c= b2 & ( S-min b2 in b1 or S-max b2 in b1 ) holds
S-bound b1 = S-bound b2
proof end;

theorem Th12: :: JORDAN:12
for b1 being Simple_closed_curve holds W-bound b1 = W-bound (North_Arc b1)
proof end;

theorem Th13: :: JORDAN:13
for b1 being Simple_closed_curve holds E-bound b1 = E-bound (North_Arc b1)
proof end;

theorem Th14: :: JORDAN:14
for b1 being Simple_closed_curve holds W-bound b1 = W-bound (South_Arc b1)
proof end;

theorem Th15: :: JORDAN:15
for b1 being Simple_closed_curve holds E-bound b1 = E-bound (South_Arc b1)
proof end;

theorem Th16: :: JORDAN:16
for b1 being real number
for b2, b3 being Point of (TOP-REAL 2) st b2 `1 <= b1 & b1 <= b3 `1 holds
LSeg b2,b3 meets Vertical_Line b1
proof end;

theorem Th17: :: JORDAN:17
for b1 being real number
for b2, b3 being Point of (TOP-REAL 2) st b2 `2 <= b1 & b1 <= b3 `2 holds
LSeg b2,b3 meets Horizontal_Line b1
proof end;

E11: now
let c2 be Nat;
let c3 be Subset of (TOP-REAL c2);
assume E12: c3 is empty ;
consider c4 being Point of (TOP-REAL c2);
c3 c= {c4} by E12, XBOOLE_1:2;
hence c3 is Bounded by JORDAN2C:16;
end;

registration
let c2 be Nat;
cluster empty -> Bounded Element of bool the carrier of (TOP-REAL a1);
coherence
for b1 being Subset of (TOP-REAL c2) st b1 is empty holds
b1 is Bounded by Lemma11;
cluster non Bounded -> non empty Element of bool the carrier of (TOP-REAL a1);
coherence
for b1 being Subset of (TOP-REAL c2) st not b1 is Bounded holds
not b1 is empty by Lemma11;
end;

registration
let c2 be non empty Nat;
cluster non empty open closed non Bounded convex Element of bool the carrier of (TOP-REAL a1);
existence
ex b1 being Subset of (TOP-REAL c2) st
( b1 is open & b1 is closed & not b1 is Bounded & b1 is convex )
proof end;
end;

theorem Th18: :: JORDAN:18
for b1 being compact Subset of (TOP-REAL 2) holds (north_halfline (UMP b1)) \ {(UMP b1)} misses b1
proof end;

theorem Th19: :: JORDAN:19
for b1 being compact Subset of (TOP-REAL 2) holds (south_halfline (LMP b1)) \ {(LMP b1)} misses b1
proof end;

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

theorem Th20: :: JORDAN:20
for b1 being compact Subset of (TOP-REAL 2) holds (north_halfline (UMP b1)) \ {(UMP b1)} c= UBD b1
proof end;

theorem Th21: :: JORDAN:21
for b1 being compact Subset of (TOP-REAL 2) holds (south_halfline (LMP b1)) \ {(LMP b1)} c= UBD b1
proof end;

theorem Th22: :: JORDAN:22
for b1, b2 being Subset of (TOP-REAL 2) st b1 is_inside_component_of b2 holds
UBD b2 misses b1
proof end;

theorem Th23: :: JORDAN:23
for b1, b2 being Subset of (TOP-REAL 2) st b1 is_outside_component_of b2 holds
BDD b2 misses b1
proof end;

Lemma18: for b1 being Point of (TOP-REAL 2)
for b2 being Simple_closed_curve
for b3 being Subset of ((TOP-REAL 2) | (b2 ` )) st b1 in b2 holds
{b1} misses b3
proof end;

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

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

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

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

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

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

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

E21: now
let c7 be non empty TopSpace;
let c8 be Real;
set c9 = the carrier of c7;
set c10 = the carrier of c7 --> c8;
thus the carrier of c7 --> c8 is continuous
proof
E22: dom (the carrier of c7 --> c8) = the carrier of c7 by FUNCT_2:def 1;
E23: rng (the carrier of c7 --> c8) = {c8} by FUNCOP_1:14;
let c11 be Subset of REAL ; :: according to PSCOMP_1:def 25
assume c11 is closed ;
per cases ( c8 in c11 or not c8 in c11 ) ;
suppose c8 in c11 ;
then E24: rng (the carrier of c7 --> c8) c= c11 by E23, ZFMISC_1:37;
(the carrier of c7 --> c8) " c11 = (the carrier of c7 --> c8) " ((rng (the carrier of c7 --> c8)) /\ c11) by RELAT_1:168
.= (the carrier of c7 --> c8) " (rng (the carrier of c7 --> c8)) by E24, XBOOLE_1:28
.= the carrier of c7 by E22, RELAT_1:169
.= [#] c7 by PRE_TOPC:12 ;
hence (the carrier of c7 --> c8) " c11 is closed ;
end;
suppose not c8 in c11 ;
then E24: rng (the carrier of c7 --> c8) misses c11 by E23, ZFMISC_1:56;
(the carrier of c7 --> c8) " c11 = (the carrier of c7 --> c8) " ((rng (the carrier of c7 --> c8)) /\ c11) by RELAT_1:168
.= (the carrier of c7 --> c8) " {} by E24, XBOOLE_0:def 7
.= {} c7 by RELAT_1:171 ;
hence (the carrier of c7 --> c8) " c11 is closed ;
end;
end;
end;
end;

theorem Th24: :: JORDAN:24
for b1 being Nat
for b2 being real positive number
for b3 being Point of (TOP-REAL b1) holds b3 in Ball b3,b2
proof end;

theorem Th25: :: JORDAN:25
for b1 being Nat
for b2 being real non negative number
for b3 being Point of (TOP-REAL b1) holds b3 is Point of (Tdisk b3,b2)
proof end;

registration
let c7 be real positive number ;
let c8 be non empty Nat;
let c9, c10 be Point of (TOP-REAL c8);
cluster (cl_Ball a3,a1) \ {a4} -> non empty ;
coherence
not (cl_Ball c9,c7) \ {c10} is empty
proof end;
end;

theorem Th26: :: JORDAN:26
for b1, b2 being real number
for b3 being Nat
for b4 being Point of (TOP-REAL b3) st b1 <= b2 holds
Ball b4,b1 c= Ball b4,b2
proof end;

theorem Th27: :: JORDAN:27
for b1 being real number
for b2 being Nat
for b3 being Point of (TOP-REAL b2) holds (cl_Ball b3,b1) \ (Ball b3,b1) = Sphere b3,b1
proof end;

theorem Th28: :: JORDAN:28
for b1 being real number
for b2 being Nat
for b3, b4 being Point of (TOP-REAL b2) st b3 in Sphere b4,b1 holds
(LSeg b4,b3) \ {b4,b3} c= Ball b4,b1
proof end;

theorem Th29: :: JORDAN:29
for b1, b2 being real number
for b3 being Nat
for b4 being Point of (TOP-REAL b3) st b1 < b2 holds
cl_Ball b4,b1 c= Ball b4,b2
proof end;

theorem Th30: :: JORDAN:30
for b1, b2 being real number
for b3 being Nat
for b4 being Point of (TOP-REAL b3) st b1 < b2 holds
Sphere b4,b1 c= Ball b4,b2
proof end;

theorem Th31: :: JORDAN:31
for b1 being Nat
for b2 being Point of (TOP-REAL b1)
for b3 being non zero real number holds Cl (Ball b2,b3) = cl_Ball b2,b3
proof end;

theorem Th32: :: JORDAN:32
for b1 being Nat
for b2 being Point of (TOP-REAL b1)
for b3 being non zero real number holds Fr (Ball b2,b3) = Sphere b2,b3
proof end;

registration
let c7 be non empty Nat;
cluster Bounded -> proper Element of bool the carrier of (TOP-REAL a1);
coherence
for b1 being Subset of (TOP-REAL c7) st b1 is Bounded holds
b1 is proper
proof end;
end;

registration
let c7 be Nat;
cluster non empty closed Bounded convex Element of bool the carrier of (TOP-REAL a1);
existence
ex b1 being Subset of (TOP-REAL c7) st
( not b1 is empty & b1 is closed & b1 is convex & b1 is Bounded )
proof end;
cluster non empty open Bounded convex Element of bool the carrier of (TOP-REAL a1);
existence
ex b1 being Subset of (TOP-REAL c7) st
( not b1 is empty & b1 is open & b1 is convex & b1 is Bounded )
proof end;
end;

registration
let c7 be Nat;
let c8 be Bounded Subset of (TOP-REAL c7);
cluster Cl a2 -> Bounded ;
coherence
Cl c8 is Bounded by TOPREAL6:71;
end;

registration
let c7 be Nat;
let c8 be Bounded Subset of (TOP-REAL c7);
cluster Fr a2 -> Bounded ;
coherence
Fr c8 is Bounded by JORDAN1I:1;
end;

theorem Th33: :: JORDAN:33
for b1 being Nat
for b2 being closed Subset of (TOP-REAL b1)
for b3 being Point of (TOP-REAL b1) st not b3 in b2 holds
ex b4 being real positive number st Ball b3,b4 misses b2
proof end;

theorem Th34: :: JORDAN:34
for b1 being Nat
for b2 being Bounded Subset of (TOP-REAL b1)
for b3 being Point of (TOP-REAL b1) ex b4 being real positive number st b2 c= Ball b3,b4
proof end;

theorem Th35: :: JORDAN:35
for b1, b2 being TopStruct
for b3 being Function of b1,b2 st b3 is_homeomorphism holds
b3 is onto
proof end;

theorem Th36: :: JORDAN:36
for b1 being TopSpace
for b2 being SubSpace of b1
for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 holds
b1 | b3 = b2 | b4
proof end;

registration
let c7 be non empty being_T2 TopSpace;
cluster non empty -> non empty being_T2 SubSpace of a1;
coherence
for b1 being non empty SubSpace of c7 holds b1 is being_T2 by TOPMETR:3;
end;

registration
let c7 be Point of (TOP-REAL 2);
let c8 be real number ;
cluster Tdisk a1,a2 -> closed ;
coherence
Tdisk c7,c8 is closed
proof end;
end;

registration
let c7 be Point of (TOP-REAL 2);
let c8 be real number ;
cluster Tdisk a1,a2 -> compact closed ;
coherence
Tdisk c7,c8 is compact
proof end;
end;

theorem Th37: :: JORDAN:37
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3 st b2,b3 are_connected holds
rng b4 is connected
proof end;

theorem Th38: :: JORDAN:38
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1
for b3, b4 being Point of b1
for b5, b6 being Point of b2
for b7 being Path of b3,b4 st b3 = b5 & b4 = b6 & b3,b4 are_connected & rng b7 c= the carrier of b2 holds
( b5,b6 are_connected & b7 is Path of b5,b6 )
proof end;

theorem Th39: :: JORDAN:39
for b1 being non empty arcwise_connected TopSpace
for b2 being non empty SubSpace of b1
for b3, b4 being Point of b1
for b5, b6 being Point of b2
for b7 being Path of b3,b4 st b3 = b5 & b4 = b6 & rng b7 c= the carrier of b2 holds
( b5,b6 are_connected & b7 is Path of b5,b6 )
proof end;

Lemma37: for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3 st b2,b3 are_connected holds
rng b4 c= rng (- b4)
proof end;

theorem Th40: :: JORDAN:40
for b1 being non empty TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3 st b2,b3 are_connected holds
rng b4 = rng (- b4)
proof end;

theorem Th41: :: JORDAN:41
for b1 being non empty arcwise_connected TopSpace
for b2, b3 being Point of b1
for b4 being Path of b2,b3 holds rng b4 = rng (- b4)
proof end;

theorem Th42: :: JORDAN:42
for b1 being non empty TopSpace
for b2, b3, b4 being Point of b1
for b5 being Path of b2,b3
for b6 being Path of b3,b4 st b2,b3 are_connected & b3,b4 are_connected holds
rng b5 c= rng (b5 + b6)
proof end;

theorem Th43: :: JORDAN:43
for b1 being non empty arcwise_connected TopSpace
for b2, b3, b4 being Point of b1
for b5 being Path of b2,b3
for b6 being Path of b3,b4 holds rng b5 c= rng (b5 + b6)
proof end;

theorem Th44: :: JORDAN:44
for b1 being non empty TopSpace
for b2, b3, b4 being Point of b1
for b5 being Path of b3,b4
for b6 being Path of b2,b3 st b2,b3 are_connected & b3,b4 are_connected holds
rng b5 c= rng (b6 + b5)
proof end;

theorem Th45: :: JORDAN:45
for b1 being non empty arcwise_connected TopSpace
for b2, b3, b4 being Point of b1
for b5 being Path of b3,b4
for b6 being Path of b2,b3 holds rng b5 c= rng (b6 + b5)
proof end;

theorem Th46: :: JORDAN:46
for b1 being non empty TopSpace
for b2, b3, b4 being Point of b1
for b5 being Path of b2,b3
for b6 being Path of b3,b4 st b2,b3 are_connected & b3,b4 are_connected holds
rng (b5 + b6) = (rng b5) \/ (rng b6)
proof end;

theorem Th47: :: JORDAN:47
for b1 being non empty arcwise_connected TopSpace
for b2, b3, b4 being Point of b1
for b5 being Path of b2,b3
for b6 being Path of b3,b4 holds rng (b5 + b6) = (rng b5) \/ (rng b6)
proof end;

theorem Th48: :: JORDAN:48
for b1 being non empty TopSpace
for b2, b3, b4, b5 being Point of b1
for b6 being Path of b2,b3
for b7 being Path of b3,b4
for b8 being Path of b4,b5 st b2,b3 are_connected & b3,b4 are_connected & b4,b5 are_connected holds
rng ((b6 + b7) + b8) = ((rng b6) \/ (rng b7)) \/ (rng b8)
proof end;

theorem Th49: :: JORDAN:49
for b1 being non empty arcwise_connected TopSpace
for b2, b3, b4, b5 being Point of b1
for b6 being Path of b2,b3
for b7 being Path of b3,b4
for b8 being Path of b4,b5 holds rng ((b6 + b7) + b8) = ((rng b6) \/ (rng b7)) \/ (rng b8)
proof end;

Lemma45: for b1 being non empty TopSpace
for b2, b3, b4, b5, b6 being Point of b1
for b7 being Path of b2,b3
for b8 being Path of b3,b4
for b9 being Path of b4,b5
for b10 being Path of b5,b6 st b2,b3 are_connected & b3,b4 are_connected & b4,b5 are_connected & b5,b6 are_connected holds
rng (((b7 + b8) + b9) + b10) = (((rng b7) \/ (rng b8)) \/ (rng b9)) \/ (rng b10)
proof end;

Lemma46: for b1 being non empty arcwise_connected TopSpace
for b2, b3, b4, b5, b6 being Point of b1
for b7 being Path of b2,b3
for b8 being Path of b3,b4
for b9 being Path of b4,b5
for b10 being Path of b5,b6 holds rng (((b7 + b8) + b9) + b10) = (((rng b7) \/ (rng b8)) \/ (rng b9)) \/ (rng b10)
proof end;

Lemma47: for b1 being non empty TopSpace
for b2, b3, b4, b5, b6, b7 being Point of b1
for b8 being Path of b2,b3
for b9 being Path of b3,b4
for b10 being Path of b4,b5
for b11 being Path of b5,b6
for b12 being Path of b6,b7 st b2,b3 are_connected & b3,b4 are_connected & b4,b5 are_connected & b5,b6 are_connected & b6,b7 are_connected holds
rng ((((b8 + b9) + b10) + b11) + b12) = ((((rng b8) \/ (rng b9)) \/ (rng b10)) \/ (rng b11)) \/ (rng b12)
proof end;

Lemma48: for b1 being non empty arcwise_connected TopSpace
for b2, b3, b4, b5, b6, b7 being Point of b1
for b8 being Path of b2,b3
for b9 being Path of b3,b4
for b10 being Path of b4,b5
for b11 being Path of b5,b6
for b12 being Path of b6,b7 holds rng ((((b8 + b9) + b10) + b11) + b12) = ((((rng b8) \/ (rng b9)) \/ (rng b10)) \/ (rng b11)) \/ (rng b12)
proof end;

theorem Th50: :: JORDAN:50
for b1 being non empty TopSpace
for b2 being Point of b1 holds I[01] --> b2 is Path of b2,b2
proof end;

theorem Th51: :: JORDAN:51
for b1 being Nat
for b2, b3 being Point of (TOP-REAL b1)
for b4 being Subset of (TOP-REAL b1) st b4 is_an_arc_of b2,b3 holds
ex b5 being Path of b2,b3ex b6 being Function of I[01] ,((TOP-REAL b1) | b4) st
( rng b6 = b4 & b5 = b6 )
proof end;

theorem Th52: :: JORDAN:52
for b1 being Nat
for b2, b3 being Point of (TOP-REAL b1) ex b4 being Path of b2,b3ex b5 being Function of I[01] ,((TOP-REAL b1) | (LSeg b2,b3)) st
( rng b5 = LSeg b2,b3 & b4 = b5 )
proof end;

theorem Th53: :: JORDAN:53
for b1 being Subset of (TOP-REAL 2)
for b2, b3, b4, b5 being Point of (TOP-REAL 2) st b1 is_an_arc_of b2,b3 & b4 in b1 & b5 in b1 & b4 <> b2 & b4 <> b3 & b5 <> b2 & b5 <> b3 holds
ex b6 being Path of b4,b5 st
( rng b6 c= b1 & rng b6 misses {b2,b3} )
proof end;

theorem Th54: :: JORDAN:54
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
rectangle b1,b2,b3,b4 c= closed_inside_of_rectangle b1,b2,b3,b4
proof end;

theorem Th55: :: JORDAN:55
for b1, b2, b3, b4 being real number holds inside_of_rectangle b1,b2,b3,b4 c= closed_inside_of_rectangle b1,b2,b3,b4
proof end;

theorem Th56: :: JORDAN:56
for b1, b2, b3, b4 being real number holds closed_inside_of_rectangle b1,b2,b3,b4 = (outside_of_rectangle b1,b2,b3,b4) `
proof end;

registration
let c7, c8, c9, c10 be real number ;
cluster closed_inside_of_rectangle a1,a2,a3,a4 -> closed ;
coherence
closed_inside_of_rectangle c7,c8,c9,c10 is closed
proof end;
end;

theorem Th57: :: JORDAN:57
for b1, b2, b3, b4 being real number holds closed_inside_of_rectangle b1,b2,b3,b4 misses outside_of_rectangle b1,b2,b3,b4
proof end;

theorem Th58: :: JORDAN:58
for b1, b2, b3, b4 being real number holds (closed_inside_of_rectangle b1,b2,b3,b4) /\ (inside_of_rectangle b1,b2,b3,b4) = inside_of_rectangle b1,b2,b3,b4
proof end;

theorem Th59: :: JORDAN:59
for b1, b2, b3, b4 being real number st b1 < b2 & b3 < b4 holds
Int (closed_inside_of_rectangle b1,b2,b3,b4) = inside_of_rectangle b1,b2,b3,b4
proof end;

theorem Th60: :: JORDAN:60
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
(closed_inside_of_rectangle b1,b2,b3,b4) \ (inside_of_rectangle b1,b2,b3,b4) = rectangle b1,b2,b3,b4
proof end;

theorem Th61: :: JORDAN:61
for b1, b2, b3, b4 being real number st b1 < b2 & b3 < b4 holds
Fr (closed_inside_of_rectangle b1,b2,b3,b4) = rectangle b1,b2,b3,b4
proof end;

theorem Th62: :: JORDAN:62
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
W-bound (closed_inside_of_rectangle b1,b2,b3,b4) = b1
proof end;

theorem Th63: :: JORDAN:63
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
S-bound (closed_inside_of_rectangle b1,b2,b3,b4) = b3
proof end;

theorem Th64: :: JORDAN:64
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
E-bound (closed_inside_of_rectangle b1,b2,b3,b4) = b2
proof end;

theorem Th65: :: JORDAN:65
for b1, b2, b3, b4 being real number st b1 <= b2 & b3 <= b4 holds
N-bound (closed_inside_of_rectangle b1,b2,b3,b4) = b4
proof end;

theorem Th66: :: JORDAN:66
for b1, b2, b3, b4 being real number
for b5, b6 being Point of (TOP-REAL 2)
for b7 being Subset of (TOP-REAL 2) st b1 < b2 & b3 < b4 & b5 in closed_inside_of_rectangle b1,b2,b3,b4 & not b6 in closed_inside_of_rectangle b1,b2,b3,b4 & b7 is_an_arc_of b5,b6 holds
Segment b7,b5,b6,b5,(First_Point b7,b5,b6,(rectangle b1,b2,b3,b4)) c= closed_inside_of_rectangle b1,b2,b3,b4
proof end;

definition
let c7, c8 be non empty TopSpace;
let c9 be Point of [:c7,c8:];
redefine func `1 as c3 `1 -> Element of a1;
coherence
c9 `1 is Element of c7
proof end;
redefine func `2 as c3 `2 -> Element of a2;
coherence
c9 `2 is Element of c8
proof end;
end;

definition
let c7 be Point of (TOP-REAL 2);
func diffX2_1 c1 -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def1: :: JORDAN:def 1
for b1 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds a2 . b1 = ((b1 `2 ) `1 ) - (a1 `1 );
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for b2 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b2 = ((b2 `2 ) `1 ) - (c7 `1 )
proof end;
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for b3 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b3 = ((b3 `2 ) `1 ) - (c7 `1 ) ) & ( for b3 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . b3 = ((b3 `2 ) `1 ) - (c7 `1 ) ) holds
b1 = b2
proof end;
func diffX2_2 c1 -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def2: :: JORDAN:def 2
for b1 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds a2 . b1 = ((b1 `2 ) `2 ) - (a1 `2 );
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for b2 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b2 = ((b2 `2 ) `2 ) - (c7 `2 )
proof end;
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for b3 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b3 = ((b3 `2 ) `2 ) - (c7 `2 ) ) & ( for b3 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . b3 = ((b3 `2 ) `2 ) - (c7 `2 ) ) holds
b1 = b2
proof end;
end;

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

:: deftheorem Def2 defines diffX2_2 JORDAN:def 2 :
for b1 being Point of (TOP-REAL 2)
for b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds
( b2 = diffX2_2 b1 iff for b3 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . b3 = ((b3 `2 ) `2 ) - (b1 `2 ) );

definition
func diffX1_X2_1 -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def3: :: JORDAN:def 3
for b1 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds a1 . b1 = ((b1 `1 ) `1 ) - ((b1 `2 ) `1 );
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for b2 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b2 = ((b2 `1 ) `1 ) - ((b2 `2 ) `1 )
proof end;
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for b3 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b3 = ((b3 `1 ) `1 ) - ((b3 `2 ) `1 ) ) & ( for b3 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . b3 = ((b3 `1 ) `1 ) - ((b3 `2 ) `1 ) ) holds
b1 = b2
proof end;
func diffX1_X2_2 -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def4: :: JORDAN:def 4
for b1 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds a1 . b1 = ((b1 `1 ) `2 ) - ((b1 `2 ) `2 );
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for b2 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b2 = ((b2 `1 ) `2 ) - ((b2 `2 ) `2 )
proof end;
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for b3 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b3 = ((b3 `1 ) `2 ) - ((b3 `2 ) `2 ) ) & ( for b3 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . b3 = ((b3 `1 ) `2 ) - ((b3 `2 ) `2 ) ) holds
b1 = b2
proof end;
func Proj2_1 -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def5: :: JORDAN:def 5
for b1 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds a1 . b1 = (b1 `2 ) `1 ;
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for b2 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b2 = (b2 `2 ) `1
proof end;
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for b3 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b3 = (b3 `2 ) `1 ) & ( for b3 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . b3 = (b3 `2 ) `1 ) holds
b1 = b2
proof end;
func Proj2_2 -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def6: :: JORDAN:def 6
for b1 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds a1 . b1 = (b1 `2 ) `2 ;
existence
ex b1 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st
for b2 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b2 = (b2 `2 ) `2
proof end;
uniqueness
for b1, b2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for b3 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b3 = (b3 `2 ) `2 ) & ( for b3 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b2 . b3 = (b3 `2 ) `2 ) holds
b1 = b2
proof end;
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 b2 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b2 = ((b2 `1 ) `1 ) - ((b2 `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 b2 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b2 = ((b2 `1 ) `2 ) - ((b2 `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 b2 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b2 = (b2 `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 b2 being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b1 . b2 = (b2 `2 ) `2 );

theorem Th67: :: JORDAN:67
for b1 being Point of (TOP-REAL 2) holds diffX2_1 b1 is continuous Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1
proof end;

theorem Th68: :: JORDAN:68
for b1 being Point of (TOP-REAL 2) holds diffX2_2 b1 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 c7 be Point of (TOP-REAL 2);
cluster diffX2_1 a1 -> continuous ;
coherence
diffX2_1 c7 is continuous
proof end;
cluster diffX2_2 a1 -> continuous ;
coherence
diffX2_2 c7 is continuous
proof end;
end;

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

definition
let c7 be non empty Nat;
let c8, c9 be Point of (TOP-REAL c7);
let c10 be real positive number ;
assume E74: c9 is Point of (Tdisk c8,c10) ;
set c11 = (TOP-REAL c7) | ((cl_Ball c8,c10) \ {c9});
func DiskProj c2,c4,c3 -> Function of ((TOP-REAL a1) | ((cl_Ball a2,a4) \ {a3})),(Tcircle a2,a4) means :Def7: :: JORDAN:def 7
for b1 being Point of ((TOP-REAL a1) | ((cl_Ball a2,a4) \ {a3})) ex b2 being Point of (TOP-REAL a1) st
( b1 = b2 & a5 . b1 = HC a3,b2,a2,a4 );
existence
ex b1 being Function of ((TOP-REAL c7) | ((cl_Ball c8,c10) \ {c9})),(Tcircle c8,c10) st
for b2 being Point of ((TOP-REAL c7) | ((cl_Ball c8,c10) \ {c9})) ex b3 being Point of (TOP-REAL c7) st
( b2 = b3 & b1 . b2 = HC c9,b3,c8,c10 )
proof end;
uniqueness
for b1, b2 being Function of ((TOP-REAL c7) | ((cl_Ball c8,c10) \ {c9})),(Tcircle c8,c10) st ( for b3 being Point of ((TOP-REAL c7) | ((cl_Ball c8,c10) \ {c9})) ex b4 being Point of (TOP-REAL c7) st
( b3 = b4 & b1 . b3 = HC c9,b4,c8,c10 ) ) & ( for b3 being Point of ((TOP-REAL c7) | ((cl_Ball c8,c10) \ {c9})) ex b4 being Point of (TOP-REAL c7) st
( b3 = b4 & b2 . b3 = HC c9,b4,c8,c10 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines DiskProj JORDAN:def 7 :
for b1 being non empty Nat
for b2, b3 being Point of (TOP-REAL b1)
for b4 being real positive number st b3 is Point of (Tdisk b2,b4) holds
for b5 being Function of ((TOP-REAL b1) | ((cl_Ball b2,b4) \ {b3})),(Tcircle b2,b4) holds
( b5 = DiskProj b2,b4,b3 iff for b6 being Point of ((TOP-REAL b1) | ((cl_Ball b2,b4) \ {b3})) ex b7 being Point of (TOP-REAL b1) st
( b6 = b7 & b5 . b6 = HC b3,b7,b2,b4 ) );

theorem Th73: :: JORDAN:73
for b1, b2 being Point of (TOP-REAL 2)
for b3 being real positive number st b2 is Point of (Tdisk b1,b3) holds
DiskProj b1,b3,b2 is continuous
proof end;

theorem Th74: :: JORDAN:74
for b1 being non empty Nat
for b2, b3 being Point of (TOP-REAL b1)
for b4 being real positive number st b3 in Ball b2,b4 holds
(DiskProj b2,b4,b3) | (Sphere b2,b4) = id (Sphere b2,b4)
proof end;

definition
let c7 be non empty Nat;
let c8, c9 be Point of (TOP-REAL c7);
let c10 be real positive number ;
assume E77: c9 in Ball c8,c10 ;
set c11 = Tcircle c8,c10;
func RotateCircle c2,c4,c3 -> Function of (Tcircle a2,a4),(Tcircle a2,a4) means :Def8: :: JORDAN:def 8
for b1 being Point of (Tcircle a2,a4) ex b2 being Point of (TOP-REAL a1) st
( b1 = b2 & a5 . b1 = HC b2,a3,a2,a4 );
existence
ex b1 being Function of (Tcircle c8,c10),(Tcircle c8,c10) st
for b2 being Point of (Tcircle c8,c10) ex b3 being Point of (TOP-REAL c7) st
( b2 = b3 & b1 . b2 = HC b3,c9,c8,c10 )
proof end;
uniqueness
for b1, b2 being Function of (Tcircle c8,c10),(Tcircle c8,c10) st ( for b3 being Point of (Tcircle c8,c10) ex b4 being Point of (TOP-REAL c7) st
( b3 = b4 & b1 . b3 = HC b4,c9,c8,c10 ) ) & ( for b3 being Point of (Tcircle c8,c10) ex b4 being Point of (TOP-REAL c7) st
( b3 = b4 & b2 . b3 = HC b4,c9,c8,c10 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines RotateCircle JORDAN:def 8 :
for b1 being non empty Nat
for b2, b3 being Point of (TOP-REAL b1)
for b4 being real positive number st b3 in Ball b2,b4 holds
for b5 being Function of (Tcircle b2,b4),(Tcircle b2,b4) holds
( b5 = RotateCircle b2,b4,b3 iff for b6 being Point of (Tcircle b2,b4) ex b7 being Point of (TOP-REAL b1) st
( b6 = b7 & b5 . b6 = HC b7,b3,b2,b4 ) );

theorem Th75: :: JORDAN:75
for b1, b2 being Point of (TOP-REAL 2)
for b3 being real positive number st b2 in Ball b1,b3 holds
RotateCircle b1,b3,b2 is continuous
proof end;

theorem Th76: :: JORDAN:76
for b1 being non empty Nat
for b2, b3 being Point of (TOP-REAL b1)
for b4 being real positive number st b3 in Ball b2,b4 holds
RotateCircle b2,b4,b3 has_no_fixpoint
proof end;

theorem Th77: :: JORDAN:77
for b1 being Simple_closed_curve
for b2 being Subset of (TOP-REAL 2)
for b3, b4 being Subset of ((TOP-REAL 2) | (b1 ` )) st b3 = b2 & b3 is_a_component_of (TOP-REAL 2) | (b1 ` ) & b4 is_a_component_of (TOP-REAL 2) | (b1 ` ) & b3 <> b4 holds
Cl b2 misses b4
proof end;

theorem Th78: :: JORDAN:78
for b1 being Simple_closed_curve
for b2 being Subset of ((TOP-REAL 2) | (b1 ` )) st b2 is_a_component_of (TOP-REAL 2) | (b1 ` ) holds
((TOP-REAL 2) | (b1 ` )) | b2 is arcwise_connected
proof end;

Lemma82: for b1, b2, b3 being Point of (TOP-REAL 2)
for b4 being Subset of (TOP-REAL 2)
for b5 being real non negative number st b4 is_an_arc_of b1,b2 & b4 is Subset of (Tdisk b3,b5) holds
ex b6 being Function of (Tdisk b3,b5),((TOP-REAL 2) | b4) st
( b6 is continuous & b6 | b4 = id b4 )
proof end;

Lemma83: for b1, b2, b3 being Point of (TOP-REAL 2)
for b4 being Simple_closed_curve
for b5, b6, b7 being Subset of (TOP-REAL 2)
for b8 being Subset of ((TOP-REAL 2) | (b4 ` ))
for b9 being real positive number st b5 is_an_arc_of b1,b2 & b5 c= b4 & b4 c= Ball b3,b9 & b3 in b8 & (Cl b6) /\ (b6 ` ) c= b5 & b6 c= Ball b3,b9 holds
for b10 being Function of (Tdisk b3,b9),((TOP-REAL 2) | b5) st b10 is continuous & b10 | b5 = id b5 & b8 = b6 & b8 is_a_component_of (TOP-REAL 2) | (b4 ` ) & b7 = (cl_Ball b3,b9) \ {b3} holds
ex b11 being Function of (Tdisk b3,b9),((TOP-REAL 2) | b7) st
( b11 is continuous & ( for b12 being Point of (Tdisk b3,b9) holds
( ( b12 in Cl b6 implies b11 . b12 = b10 . b12 ) & ( b12 in b6 ` implies b11 . b12 = b12 ) ) ) )
proof end;

Lemma84: for b1 being Point of (TOP-REAL 2)
for b2 being Simple_closed_curve
for b3, b4 being Subset of (TOP-REAL 2)
for b5, b6 being Subset of ((TOP-REAL 2) | (b2 ` ))
for b7 being non empty Subset of (TOP-REAL 2)
for b8 being Subset of (TOP-REAL 2) st b5 <> b6 holds
for b9 being real positive number st b7 c= b2 & b2 c= Ball b1,b9 & b1 in b6 & (Cl b3) /\ (b3 ` ) c= b7 & Ball b1,b9 meets b3 holds
for b10 being Function of (Tdisk b1,b9),((TOP-REAL 2) | b7) st b10 is continuous & b10 | b7 = id b7 & b5 = b3 & b5 is_a_component_of (TOP-REAL 2) | (b2 ` ) & b6 is_a_component_of (TOP-REAL 2) | (b2 ` ) & b4 = (cl_Ball b1,b9) \ {b1} holds
ex b11 being Function of (Tdisk b1,b9),((TOP-REAL 2) | b4) st
( b11 is continuous & ( for b12 being Point of (Tdisk b1,b9) holds
( ( b12 in Cl b3 implies b11 . b12 = b12 ) & ( b12 in b3 ` implies b11 . b12 = b10 . b12 ) ) ) )
proof end;

theorem Th79: :: JORDAN:79
for b1 being Simple_closed_curve
for b2 being Subset of (TOP-REAL 2)
for b3 being Subset of ((TOP-REAL 2) | (b1 ` )) st b3 = b2 & b3 is_a_component_of (TOP-REAL 2) | (b1 ` ) holds
b1 = Fr b2
proof end;

set c7 = 1;

set c8 = - 1;

set c9 = 3;

set c10 = - 3;

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

set c12 = |[1,0]|;

set c13 = |[0,3]|;

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

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

set c16 = |[1,3]|;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma106: 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 Lemma106, XBOOLE_1:7;

then Lemma107: 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 Lemma106, XBOOLE_1:7;

then Lemma108: 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 Lemma106, XBOOLE_1:7;

then Lemma109: 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 Lemma106, XBOOLE_1:7;

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

Lemma111: LSeg |[(- 1),(- 3)]|,|[(- 1),3]| is vertical
by Lemma94, Lemma96, SPPOL_1:37;

Lemma112: LSeg |[1,(- 3)]|,|[1,3]| is vertical
by Lemma98, Lemma100, SPPOL_1:37;

Lemma113: LSeg |[(- 1),0]|,|[(- 1),3]| is vertical
by Lemma86, Lemma94, SPPOL_1:37;

Lemma114: LSeg |[(- 1),0]|,|[(- 1),(- 3)]| is vertical
by Lemma86, Lemma96, SPPOL_1:37;

Lemma115: LSeg |[1,0]|,|[1,3]| is vertical
by Lemma87, Lemma98, SPPOL_1:37;

Lemma116: LSeg |[1,0]|,|[1,(- 3)]| is vertical
by Lemma87, Lemma100, SPPOL_1:37;

Lemma117: LSeg |[(- 1),(- 3)]|,|[0,(- 3)]| is horizontal
by Lemma97, Lemma93, SPPOL_1:36;

Lemma118: LSeg |[1,(- 3)]|,|[0,(- 3)]| is horizontal
by Lemma101, Lemma93, SPPOL_1:36;

Lemma119: LSeg |[(- 1),3]|,|[0,3]| is horizontal
by Lemma95, Lemma91, SPPOL_1:36;

Lemma120: LSeg |[1,3]|,|[0,3]| is horizontal
by Lemma99, Lemma91, SPPOL_1:36;

Lemma121: LSeg |[(- 1),3]|,|[1,3]| is horizontal
by Lemma95, Lemma99, SPPOL_1:36;

Lemma122: LSeg |[(- 1),(- 3)]|,|[1,(- 3)]| is horizontal
by Lemma97, Lemma101, SPPOL_1:36;

Lemma123: LSeg |[(- 1),0]|,|[(- 1),3]| c= LSeg |[(- 1),(- 3)]|,|[(- 1),3]|
by Lemma111, Lemma113, Lemma86, Lemma96, Lemma88, Lemma95, Lemma97, JORDAN15:5;

Lemma124: LSeg |[(- 1),0]|,|[(- 1),(- 3)]| c= LSeg |[(- 1),(- 3)]|,|[(- 1),3]|
by Lemma111, Lemma114, Lemma96, Lemma88, Lemma95, Lemma97, JORDAN15:5;

Lemma125: LSeg |[1,0]|,|[1,3]| c= LSeg |[1,(- 3)]|,|[1,3]|
by Lemma115, Lemma112, Lemma87, Lemma100, Lemma99, Lemma101, Lemma89, JORDAN15:5;

Lemma126: LSeg |[1,0]|,|[1,(- 3)]| c= LSeg |[1,(- 3)]|,|[1,3]|
by Lemma116, Lemma112, Lemma100, Lemma89, Lemma99, Lemma101, JORDAN15:5;

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

then Lemma128: |[0,3]| in rectangle (- 1),1,(- 3),3
by Lemma90, Lemma91;

Lemma129: |[0,(- 3)]| in rectangle (- 1),1,(- 3),3
by Lemma92, Lemma93, Lemma127;

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

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

E132: 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 Lemma86, Lemma87, Lemma88, Lemma89, SQUARE_1:90 ;

theorem Th80: :: JORDAN:80
for b1 being Simple_closed_curve
for b2 being Homeomorphism of TOP-REAL 2 holds b2 .: b1 is being_simple_closed_curve
proof end;

theorem Th81: :: JORDAN:81
for b1 being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
b1 c= closed_inside_of_rectangle (- 1),1,(- 3),3
proof end;

Lemma135: 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 Lemma94, Lemma98, EUCLID:56;

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

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

LSeg |[1,3]|,|[0,3]| c= LSeg |[(- 1),3]|,|[1,3]|
by Lemma120, Lemma121, Lemma90, Lemma91, Lemma94, Lemma95, Lemma98, JORDAN15:6;

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

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

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

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

LSeg |[1,(- 3)]|,|[0,(- 3)]| c= LSeg |[(- 1),(- 3)]|,|[1,(- 3)]|
by Lemma118, Lemma122, Lemma92, Lemma93, Lemma96, Lemma97, Lemma100, JORDAN15:6;

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

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

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

theorem Th82: :: JORDAN:82
for b1 being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
b1 misses LSeg |[(- 1),3]|,|[1,3]|
proof end;

theorem Th83: :: JORDAN:83
for b1 being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
b1 misses LSeg |[(- 1),(- 3)]|,|[1,(- 3)]|
proof end;

theorem Th84: :: JORDAN:84
for b1 being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
b1 /\ (rectangle (- 1),1,(- 3),3) = {|[(- 1),0]|,|[1,0]|}
proof end;

Lemma145: for b1 being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
LSeg |[(- 1),3]|,|[0,3]| misses b1
proof end;

Lemma146: for b1 being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
LSeg |[1,3]|,|[0,3]| misses b1
proof end;

Lemma147: for b1 being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
LSeg |[(- 1),(- 3)]|,|[0,(- 3)]| misses b1
proof end;

Lemma148: for b1 being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
LSeg |[1,(- 3)]|,|[0,(- 3)]| misses b1
proof end;

Lemma149: for b1 being Point of (TOP-REAL 2)
for b2 being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in b2 & b1 in b2 ` & b1 in LSeg |[(- 1),0]|,|[(- 1),3]| holds
LSeg b1,|[(- 1),3]| misses b2
proof end;

Lemma150: for b1 being Point of (TOP-REAL 2)
for b2 being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in b2 & b1 in b2 ` & b1 in LSeg |[1,0]|,|[1,3]| holds
LSeg b1,|[1,3]| misses b2
proof end;

Lemma151: for b1 being Point of (TOP-REAL 2)
for b2 being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in b2 & b1 in b2 ` & b1 in LSeg |[(- 1),0]|,|[(- 1),(- 3)]| holds
LSeg b1,|[(- 1),(- 3)]| misses b2
proof end;

Lemma152: for b1 being Point of (TOP-REAL 2)
for b2 being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in b2 & b1 in b2 ` & b1 in LSeg |[1,0]|,|[1,(- 3)]| holds
LSeg b1,|[1,(- 3)]| misses b2
proof end;

Lemma153: for b1 being real number holds
( not |[0,b1]| in rectangle (- 1),1,(- 3),3 or b1 = - 3 or b1 = 3 )
proof end;

theorem Th85: :: JORDAN:85
for b1 being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
W-bound b1 = - 1
proof end;

theorem Th86: :: JORDAN:86
for b1 being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
E-bound b1 = 1
proof end;

theorem Th87: :: JORDAN:87
for b1 being compact Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
W-most b1 = {|[(- 1),0]|}
proof end;

theorem Th88: :: JORDAN:88
for b1 being compact Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
E-most b1 = {|[1,0]|}
proof end;

theorem Th89: :: JORDAN:89
for b1 being compact Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
( W-min b1 = |[(- 1),0]| & W-max b1 = |[(- 1),0]| )
proof end;

theorem Th90: :: JORDAN:90
for b1 being compact Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
( E-min b1 = |[1,0]| & E-max b1 = |[1,0]| )
proof end;

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

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

theorem Th91: :: JORDAN:91
for b1 being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
LSeg |[0,3]|,(UMP b1) is vertical
proof end;

theorem Th92: :: JORDAN:92
for b1 being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
LSeg (LMP b1),|[0,(- 3)]| is vertical
proof end;

theorem Th93: :: JORDAN:93
for b1 being Point of (TOP-REAL 2)
for b2 being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b2 & b1 in b2 holds
b1 `2 < 3
proof end;

theorem Th94: :: JORDAN:94
for b1 being Point of (TOP-REAL 2)
for b2 being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b2 & b1 in b2 holds
- 3 < b1 `2
proof end;

theorem Th95: :: JORDAN:95
for b1 being Point of (TOP-REAL 2)
for b2 being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b2 & b1 in LSeg |[0,3]|,(UMP b2) holds
(UMP b2) `2 <= b1 `2
proof end;

theorem Th96: :: JORDAN:96
for b1 being Point of (TOP-REAL 2)
for b2 being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b2 & b1 in LSeg (LMP b2),|[0,(- 3)]| holds
b1 `2 <= (LMP b2) `2
proof end;

theorem Th97: :: JORDAN:97
for b1 being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
LSeg |[0,3]|,(UMP b1) c= north_halfline (UMP b1)
proof end;

theorem Th98: :: JORDAN:98
for b1 being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
LSeg (LMP b1),|[0,(- 3)]| c= south_halfline (LMP b1)
proof end;

theorem Th99: :: JORDAN:99
for b1 being Simple_closed_curve
for b2 being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 & b2 is_inside_component_of b1 holds
LSeg |[0,3]|,(UMP b1) misses b2
proof end;

theorem Th100: :: JORDAN:100
for b1 being Simple_closed_curve
for b2 being Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 & b2 is_inside_component_of b1 holds
LSeg (LMP b1),|[0,(- 3)]| misses b2
proof end;

theorem Th101: :: JORDAN:101
for b1 being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
(LSeg |[0,3]|,(UMP b1)) /\ b1 = {(UMP b1)}
proof end;

theorem Th102: :: JORDAN:102
for b1 being compact with_the_max_arc Subset of (TOP-REAL 2) st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
(LSeg |[0,(- 3)]|,(LMP b1)) /\ b1 = {(LMP b1)}
proof end;

theorem Th103: :: JORDAN:103
for b1, b2 being Subset of (TOP-REAL 2) st b1 is compact & |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 & b2 is_inside_component_of b1 holds
b2 c= closed_inside_of_rectangle (- 1),1,(- 3),3
proof end;

Lemma174: for b1 being Point of (TOP-REAL 2) st b1 in closed_inside_of_rectangle (- 1),1,(- 3),3 holds
closed_inside_of_rectangle (- 1),1,(- 3),3 c= Ball b1,10
proof end;

theorem Th104: :: JORDAN:104
for b1 being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
LSeg |[0,3]|,|[0,(- 3)]| meets b1
proof end;

Lemma175: for b1 being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
ex b2, b3 being compact with_the_max_arc Subset of (TOP-REAL 2) st
( b2 is_an_arc_of |[(- 1),0]|,|[1,0]| & b3 is_an_arc_of |[(- 1),0]|,|[1,0]| & b1 = b2 \/ b3 & b2 /\ b3 = {|[(- 1),0]|,|[1,0]|} & UMP b1 in b2 & LMP b1 in b3 & W-bound b1 = W-bound b2 & E-bound b1 = E-bound b2 )
proof end;

theorem Th105: :: JORDAN:105
for b1 being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
for b2, b3 being compact with_the_max_arc Subset of (TOP-REAL 2) st b2 is_an_arc_of |[(- 1),0]|,|[1,0]| & b3 is_an_arc_of |[(- 1),0]|,|[1,0]| & b1 = b2 \/ b3 & b2 /\ b3 = {|[(- 1),0]|,|[1,0]|} & UMP b1 in b2 & LMP b1 in b3 & W-bound b1 = W-bound b2 & E-bound b1 = E-bound b2 holds
for b4 being Subset of (TOP-REAL 2) st b4 = skl (Down ((1 / 2) * ((UMP ((LSeg (LMP b2),|[0,(- 3)]|) /\ b3)) + (LMP b2))),(b1 ` )) holds
( b4 is_inside_component_of b1 & ( for b5 being Subset of (TOP-REAL 2) st b5 is_inside_component_of b1 holds
b5 = b4 ) )
proof end;

theorem Th106: :: JORDAN:106
for b1 being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
for b2, b3 being compact with_the_max_arc Subset of (TOP-REAL 2) st b2 is_an_arc_of |[(- 1),0]|,|[1,0]| & b3 is_an_arc_of |[(- 1),0]|,|[1,0]| & b1 = b2 \/ b3 & b2 /\ b3 = {|[(- 1),0]|,|[1,0]|} & UMP b1 in b2 & LMP b1 in b3 & W-bound b1 = W-bound b2 & E-bound b1 = E-bound b2 holds
BDD b1 = skl (Down ((1 / 2) * ((UMP ((LSeg (LMP b2),|[0,(- 3)]|) /\ b3)) + (LMP b2))),(b1 ` ))
proof end;

Lemma178: for b1 being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in b1 holds
b1 is Jordan
proof end;

Lemma179: for b1 being Simple_closed_curve holds b1 is Jordan
proof end;

theorem Th107: :: JORDAN:107
for b1 being Simple_closed_curve ex b2, b3 being Subset of (TOP-REAL 2) st
( b1 ` = b2 \/ b3 & b2 misses b3 & (Cl b2) \ b2 = (Cl b3) \ b3 & ( for b4, b5 being Subset of ((TOP-REAL 2) | (b1 ` )) st b4 = b2 & b5 = b3 holds
( b4 is_a_component_of (TOP-REAL 2) | (b1 ` ) & b5 is_a_component_of (TOP-REAL 2) | (b1 ` ) ) ) )
proof end;

theorem Th108: :: JORDAN:108
for b1 being Simple_closed_curve holds b1 is Jordan by Lemma179;