:: by Artur Korni{\l}owicz

::

:: Received September 15, 2005

:: Copyright (c) 2005-2019 Association of Mizar Users

set T2 = TOP-REAL 2;

Lm1: for A, B, C, Z being set st A c= Z & B c= Z & C c= Z holds

(A \/ B) \/ C c= Z

proof end;

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

((A \/ B) \/ C) \/ D c= Z

proof end;

Lm3: for A, B, C, D, Z being set st A misses Z & B misses Z & C misses Z & D misses Z holds

((A \/ B) \/ C) \/ D misses Z

proof end;

registration

let M be Reflexive symmetric triangle MetrStruct ;

let x, y be Point of M;

coherence

not dist (x,y) is negative by METRIC_1:5;

end;
let x, y be Point of M;

coherence

not dist (x,y) is negative by METRIC_1:5;

registration

let n be Element of NAT ;

let x, y be Point of (TOP-REAL n);

coherence

not dist (x,y) is negative

end;
let x, y be Point of (TOP-REAL n);

coherence

not dist (x,y) is negative

proof 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

for p1, p2 being Point of (TOP-REAL n) st p1 <> p2 holds

(1 / 2) * (p1 + p2) <> p1

proof end;

theorem Th4: :: JORDAN:4

for B being Subset of (TOP-REAL 2)

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

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

proof end;

theorem :: JORDAN:5

for B being Subset of (TOP-REAL 2)

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

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

proof end;

theorem :: JORDAN:6

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

LSeg (p,p2) is vertical

LSeg (p,p2) is vertical

proof end;

theorem :: JORDAN:7

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

LSeg (p,p2) is horizontal

LSeg (p,p2) is horizontal

proof end;

registration

let P be Subset of (TOP-REAL 2);

coherence

LSeg ((SW-corner P),(SE-corner P)) is horizontal

LSeg ((NW-corner P),(SW-corner P)) is vertical

LSeg ((NE-corner P),(SE-corner P)) is vertical

end;
coherence

LSeg ((SW-corner P),(SE-corner P)) is horizontal

proof end;

coherence LSeg ((NW-corner P),(SW-corner P)) is vertical

proof end;

coherence LSeg ((NE-corner P),(SE-corner P)) is vertical

proof end;

registration

let P be Subset of (TOP-REAL 2);

coherence

LSeg ((SE-corner P),(SW-corner P)) is horizontal ;

coherence

LSeg ((SW-corner P),(NW-corner P)) is vertical ;

coherence

LSeg ((SE-corner P),(NE-corner P)) is vertical ;

end;
coherence

LSeg ((SE-corner P),(SW-corner P)) is horizontal ;

coherence

LSeg ((SW-corner P),(NW-corner P)) is vertical ;

coherence

LSeg ((SE-corner P),(NE-corner P)) is vertical ;

registration

for b_{1} being Subset of (TOP-REAL 2) st b_{1} is vertical & not b_{1} is empty & b_{1} is compact holds

b_{1} is with_the_max_arc
end;

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

coherence for b

b

proof end;

theorem Th8: :: JORDAN:8

for r being Real

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

LSeg (p1,p2) meets Vertical_Line r

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

LSeg (p1,p2) meets Vertical_Line r

proof end;

theorem :: JORDAN:9

for r being Real

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

LSeg (p1,p2) meets Horizontal_Line r

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

LSeg (p1,p2) meets Horizontal_Line r

proof end;

registration

let n be Element of NAT ;

coherence

for b_{1} being Subset of (TOP-REAL n) st b_{1} is empty holds

b_{1} is bounded
;

coherence

for b_{1} being Subset of (TOP-REAL n) st not b_{1} is bounded holds

not b_{1} is empty
;

end;
coherence

for b

b

coherence

for b

not b

registration

let n be non zero Nat;

existence

ex b_{1} being Subset of (TOP-REAL n) st

( b_{1} is open & b_{1} is closed & not b_{1} is bounded & b_{1} is convex )

end;
existence

ex b

( b

proof end;

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

proof end;

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

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

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

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

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

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 Element of REAL holds the carrier of T --> a is continuous

for a being Element of REAL holds the carrier of T --> a is continuous

let T be non empty TopSpace; :: thesis: for a being Element of REAL holds the carrier of T --> a is continuous

let a be Element of 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

end;
let a be Element of 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 to PSCOMP_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

end;
A2: rng ( the carrier of T --> a) = {a} by FUNCOP_1:8;

let Y be Subset of REAL; :: according to PSCOMP_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

per cases
( a in Y or not a in Y )
;

end;

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

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

.= {} T ;

hence ( the carrier of T --> a) " Y is closed ; :: thesis: verum

end;
( 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

.= {} T ;

hence ( the carrier of T --> a) " Y is closed ; :: thesis: verum

theorem Th17: :: JORDAN:17

for n being Element of NAT

for r being non negative Real

for p being Point of (TOP-REAL n) holds p is Point of (Tdisk (p,r))

for r being non negative Real

for p being Point of (TOP-REAL n) holds p is Point of (Tdisk (p,r))

proof end;

registration

let r be positive Real;

let n be non zero Element of NAT ;

let p, q be Point of (TOP-REAL n);

coherence

not (cl_Ball (p,r)) \ {q} is empty

end;
let n be non zero Element of NAT ;

let p, q be Point of (TOP-REAL n);

coherence

not (cl_Ball (p,r)) \ {q} is empty

proof end;

theorem Th18: :: JORDAN:18

for r, s being Real

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)

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)

proof end;

theorem Th19: :: JORDAN:19

for r being Real

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)

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)

proof end;

theorem Th20: :: JORDAN:20

for r being Real

for n being Element of NAT

for x, y being Point of (TOP-REAL n) st y in Sphere (x,r) holds

(LSeg (x,y)) \ {x,y} c= Ball (x,r)

for n being Element of NAT

for x, y being Point of (TOP-REAL n) st y in Sphere (x,r) holds

(LSeg (x,y)) \ {x,y} c= Ball (x,r)

proof end;

theorem Th21: :: JORDAN:21

for r, s being Real

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)

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)

proof end;

theorem Th22: :: JORDAN:22

for r, s being Real

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)

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)

proof end;

theorem Th23: :: JORDAN:23

for n being Element of NAT

for x being Point of (TOP-REAL n)

for r being non zero Real holds Cl (Ball (x,r)) = cl_Ball (x,r)

for x being Point of (TOP-REAL n)

for r being non zero Real holds Cl (Ball (x,r)) = cl_Ball (x,r)

proof end;

theorem Th24: :: JORDAN:24

for n being Element of NAT

for x being Point of (TOP-REAL n)

for r being non zero Real holds Fr (Ball (x,r)) = Sphere (x,r)

for x being Point of (TOP-REAL n)

for r being non zero Real holds Fr (Ball (x,r)) = Sphere (x,r)

proof end;

registration

let n be non zero Element of NAT ;

coherence

for b_{1} being Subset of (TOP-REAL n) st b_{1} is bounded holds

b_{1} is proper

end;
coherence

for b

b

proof end;

registration

let n be Element of NAT ;

existence

ex b_{1} being Subset of (TOP-REAL n) st

( not b_{1} is empty & b_{1} is closed & b_{1} is convex & b_{1} is bounded )

ex b_{1} being Subset of (TOP-REAL n) st

( not b_{1} is empty & b_{1} is open & b_{1} is convex & b_{1} is bounded )

end;
existence

ex b

( not b

proof end;

existence ex b

( not b

proof end;

registration

let n be Element of NAT ;

let A be bounded Subset of (TOP-REAL n);

coherence

Cl A is bounded by TOPREAL6:63;

end;
let A be bounded Subset of (TOP-REAL n);

coherence

Cl A is bounded by TOPREAL6:63;

registration

let n be Element of NAT ;

let A be bounded Subset of (TOP-REAL n);

coherence

Fr A is bounded by TOPREAL6:89;

end;
let A be bounded Subset of (TOP-REAL n);

coherence

Fr A is bounded by TOPREAL6:89;

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 st Ball (p,r) misses A

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 st Ball (p,r) misses A

proof end;

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 st A c= Ball (a,r)

for A being bounded Subset of (TOP-REAL n)

for a being Point of (TOP-REAL n) ex r being positive Real st A c= Ball (a,r)

proof end;

theorem :: JORDAN:27

registration

let T be non empty T_2 TopSpace;

coherence

for b_{1} being non empty SubSpace of T holds b_{1} is T_2
;

end;
coherence

for b

registration
end;

registration
end;

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

for a, b being Point of T

for f being Path of a,b st a,b are_connected holds

rng f is connected

proof end;

theorem 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 & x2 = y2 & x1,x2 are_connected & rng f c= the carrier of Y holds

( y1,y2 are_connected & f is Path of y1,y2 )

for Y being non empty SubSpace of X

for x1, x2 being Point of X

for y1, y2 being Point of Y

for f being Path of x1,x2 st x1 = y1 & x2 = y2 & x1,x2 are_connected & rng f c= the carrier of Y holds

( y1,y2 are_connected & f is Path of y1,y2 )

proof end;

theorem 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 & x2 = y2 & rng f c= the carrier of Y holds

( y1,y2 are_connected & f is Path of y1,y2 )

for Y being non empty SubSpace of X

for x1, x2 being Point of X

for y1, y2 being Point of Y

for f being Path of x1,x2 st x1 = y1 & x2 = y2 & rng f c= the carrier of Y holds

( y1,y2 are_connected & f is Path of y1,y2 )

proof end;

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)

proof end;

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)

for a, b being Point of T

for f being Path of a,b st a,b are_connected holds

rng f = rng (- f)

proof end;

theorem 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 & b,c are_connected holds

rng f c= rng (f + g)

for a, b, c being Point of T

for f being Path of a,b

for g being Path of b,c st a,b are_connected & b,c are_connected holds

rng f c= rng (f + g)

proof end;

theorem :: JORDAN: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)

for a, b, c being Point of T

for f being Path of a,b

for g being Path of b,c holds rng f c= rng (f + g)

proof end;

theorem 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 & b,c are_connected holds

rng f c= rng (g + f)

for a, b, c being Point of T

for f being Path of b,c

for g being Path of a,b st a,b are_connected & b,c are_connected holds

rng f c= rng (g + f)

proof end;

theorem :: JORDAN: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)

for a, b, c being Point of T

for f being Path of b,c

for g being Path of a,b holds rng f c= rng (g + f)

proof end;

theorem 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 & b,c are_connected holds

rng (f + g) = (rng f) \/ (rng g)

for a, b, c being Point of T

for f being Path of a,b

for g being Path of b,c st a,b are_connected & b,c are_connected holds

rng (f + g) = (rng f) \/ (rng g)

proof end;

theorem :: JORDAN: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)

for a, b, c being Point of T

for f being Path of a,b

for g being Path of b,c holds rng (f + g) = (rng f) \/ (rng g)

proof end;

theorem 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 & b,c are_connected & c,d are_connected holds

rng ((f + g) + h) = ((rng f) \/ (rng g)) \/ (rng h)

for a, b, c, d being Point of T

for f being Path of a,b

for g being Path of b,c

for h being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds

rng ((f + g) + h) = ((rng f) \/ (rng g)) \/ (rng h)

proof end;

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

for a, b, c, d being Point of T

for f being Path of a,b

for g being Path of b,c

for h being Path of c,d holds rng ((f + g) + h) = ((rng f) \/ (rng g)) \/ (rng h)

proof end;

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 & b,c are_connected & c,d are_connected & d,e are_connected holds

rng (((f + g) + h) + i) = (((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)

proof end;

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)

proof end;

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 & b,c are_connected & c,d are_connected & d,e are_connected & e,z are_connected holds

rng ((((f + g) + h) + i) + j) = ((((rng f) \/ (rng g)) \/ (rng h)) \/ (rng i)) \/ (rng j)

proof end;

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)

proof end;

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 & F = f )

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

for P being Subset of (TOP-REAL n) st P is_an_arc_of p1,p2 holds

ex F being Path of p1,p2 ex f being Function of I[01],((TOP-REAL n) | P) st

( rng f = P & F = f )

proof end;

theorem 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) & F = f )

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

( rng f = LSeg (p1,p2) & F = f )

proof end;

theorem 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 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 holds

ex f being Path of q1,q2 st

( rng f c= P & rng f misses {p1,p2} )

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & q1 in P & q2 in P & q1 <> p1 & q1 <> p2 & q2 <> p1 & q2 <> p2 holds

ex f being Path of q1,q2 st

( rng f c= P & rng f misses {p1,p2} )

proof end;

theorem Th45: :: JORDAN:45

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

rectangle (a,b,c,d) c= closed_inside_of_rectangle (a,b,c,d)

rectangle (a,b,c,d) c= closed_inside_of_rectangle (a,b,c,d)

proof end;

theorem Th46: :: JORDAN:46

for a, b, c, d being Real holds inside_of_rectangle (a,b,c,d) c= closed_inside_of_rectangle (a,b,c,d)

proof end;

theorem Th47: :: JORDAN:47

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

proof end;

registration
end;

theorem Th48: :: JORDAN:48

for a, b, c, d being Real holds closed_inside_of_rectangle (a,b,c,d) misses outside_of_rectangle (a,b,c,d)

proof end;

theorem Th49: :: JORDAN:49

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

proof end;

theorem Th50: :: JORDAN:50

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

Int (closed_inside_of_rectangle (a,b,c,d)) = inside_of_rectangle (a,b,c,d)

Int (closed_inside_of_rectangle (a,b,c,d)) = inside_of_rectangle (a,b,c,d)

proof end;

theorem Th51: :: JORDAN:51

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

(closed_inside_of_rectangle (a,b,c,d)) \ (inside_of_rectangle (a,b,c,d)) = rectangle (a,b,c,d)

(closed_inside_of_rectangle (a,b,c,d)) \ (inside_of_rectangle (a,b,c,d)) = rectangle (a,b,c,d)

proof end;

theorem Th52: :: JORDAN:52

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

Fr (closed_inside_of_rectangle (a,b,c,d)) = rectangle (a,b,c,d)

Fr (closed_inside_of_rectangle (a,b,c,d)) = rectangle (a,b,c,d)

proof end;

theorem :: JORDAN:53

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

W-bound (closed_inside_of_rectangle (a,b,c,d)) = a

W-bound (closed_inside_of_rectangle (a,b,c,d)) = a

proof end;

theorem :: JORDAN:54

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

S-bound (closed_inside_of_rectangle (a,b,c,d)) = c

S-bound (closed_inside_of_rectangle (a,b,c,d)) = c

proof end;

theorem :: JORDAN:55

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

E-bound (closed_inside_of_rectangle (a,b,c,d)) = b

E-bound (closed_inside_of_rectangle (a,b,c,d)) = b

proof end;

theorem :: JORDAN:56

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

N-bound (closed_inside_of_rectangle (a,b,c,d)) = d

N-bound (closed_inside_of_rectangle (a,b,c,d)) = d

proof end;

theorem Th57: :: JORDAN:57

for a, b, c, d being Real

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

for P being Subset of (TOP-REAL 2) st a < b & c < d & p1 in closed_inside_of_rectangle (a,b,c,d) & not p2 in closed_inside_of_rectangle (a,b,c,d) & P is_an_arc_of p1,p2 holds

Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) c= closed_inside_of_rectangle (a,b,c,d)

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

for P being Subset of (TOP-REAL 2) st a < b & c < d & p1 in closed_inside_of_rectangle (a,b,c,d) & not p2 in closed_inside_of_rectangle (a,b,c,d) & P is_an_arc_of p1,p2 holds

Segment (P,p1,p2,p1,(First_Point (P,p1,p2,(rectangle (a,b,c,d))))) c= closed_inside_of_rectangle (a,b,c,d)

proof end;

definition

let S, T be non empty TopSpace;

let x be Point of [:S,T:];

:: original: `1

redefine func x `1 -> Element of S;

coherence

x `1 is Element of S

redefine func x `2 -> Element of T;

coherence

x `2 is Element of T

end;
let x be Point of [:S,T:];

:: original: `1

redefine func x `1 -> Element of S;

coherence

x `1 is Element of S

proof end;

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

coherence

x `2 is Element of T

proof end;

definition

let o be Point of (TOP-REAL 2);

ex b_{1} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = ((x `2) `1) - (o `1)

for b_{1}, b_{2} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = ((x `2) `1) - (o `1) ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{2} . x = ((x `2) `1) - (o `1) ) holds

b_{1} = b_{2}

ex b_{1} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = ((x `2) `2) - (o `2)

for b_{1}, b_{2} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = ((x `2) `2) - (o `2) ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{2} . x = ((x `2) `2) - (o `2) ) holds

b_{1} = b_{2}

end;
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 for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = ((x `2) `1) - (o `1);

ex b

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b

proof end;

uniqueness for b

b

proof end;

func diffX2_2 o -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def2: :: JORDAN:def 2

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = ((x `2) `2) - (o `2);

existence for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = ((x `2) `2) - (o `2);

ex b

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines diffX2_1 JORDAN:def 1 :

for o being Point of (TOP-REAL 2)

for b_{2} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds

( b_{2} = diffX2_1 o iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{2} . x = ((x `2) `1) - (o `1) );

for o being Point of (TOP-REAL 2)

for b

( b

:: deftheorem Def2 defines diffX2_2 JORDAN:def 2 :

for o being Point of (TOP-REAL 2)

for b_{2} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds

( b_{2} = diffX2_2 o iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{2} . x = ((x `2) `2) - (o `2) );

for o being Point of (TOP-REAL 2)

for b

( b

definition

ex b_{1} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = ((x `1) `1) - ((x `2) `1)

for b_{1}, b_{2} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = ((x `1) `1) - ((x `2) `1) ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{2} . x = ((x `1) `1) - ((x `2) `1) ) holds

b_{1} = b_{2}

ex b_{1} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = ((x `1) `2) - ((x `2) `2)

for b_{1}, b_{2} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = ((x `1) `2) - ((x `2) `2) ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{2} . x = ((x `1) `2) - ((x `2) `2) ) holds

b_{1} = b_{2}

ex b_{1} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = (x `2) `1

for b_{1}, b_{2} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = (x `2) `1 ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{2} . x = (x `2) `1 ) holds

b_{1} = b_{2}

ex b_{1} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = (x `2) `2

for b_{1}, b_{2} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] st ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = (x `2) `2 ) & ( for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{2} . x = (x `2) `2 ) holds

b_{1} = b_{2}
end;

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 for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = ((x `1) `1) - ((x `2) `1);

ex b

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b

proof end;

uniqueness for b

b

proof end;

func diffX1_X2_2 -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def4: :: JORDAN:def 4

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = ((x `1) `2) - ((x `2) `2);

existence for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = ((x `1) `2) - ((x `2) `2);

ex b

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b

proof end;

uniqueness for b

b

proof end;

func Proj2_1 -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def5: :: JORDAN:def 5

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = (x `2) `1 ;

existence for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = (x `2) `1 ;

ex b

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b

proof end;

uniqueness for b

b

proof end;

func Proj2_2 -> RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] means :Def6: :: JORDAN:def 6

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = (x `2) `2 ;

existence for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds it . x = (x `2) `2 ;

ex b

for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines diffX1_X2_1 JORDAN:def 3 :

for b_{1} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds

( b_{1} = diffX1_X2_1 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = ((x `1) `1) - ((x `2) `1) );

for b

( b

:: deftheorem Def4 defines diffX1_X2_2 JORDAN:def 4 :

for b_{1} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds

( b_{1} = diffX1_X2_2 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = ((x `1) `2) - ((x `2) `2) );

for b

( b

:: deftheorem Def5 defines Proj2_1 JORDAN:def 5 :

for b_{1} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds

( b_{1} = Proj2_1 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = (x `2) `1 );

for b

( b

:: deftheorem Def6 defines Proj2_2 JORDAN:def 6 :

for b_{1} being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] holds

( b_{1} = Proj2_2 iff for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds b_{1} . x = (x `2) `2 );

for b

( b

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

proof end;

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

proof end;

registration

let o be Point of (TOP-REAL 2);

coherence

diffX2_1 o is continuous

diffX2_2 o is continuous

end;
coherence

diffX2_1 o is continuous

proof end;

coherence diffX2_2 o is continuous

proof end;

registration

coherence

diffX1_X2_1 is continuous by Th60, JORDAN5A:27;

coherence

diffX1_X2_2 is continuous by Th61, JORDAN5A:27;

coherence

Proj2_1 is continuous by Th62, JORDAN5A:27;

coherence

Proj2_2 is continuous by Th63, JORDAN5A:27;

end;
diffX1_X2_1 is continuous by Th60, JORDAN5A:27;

coherence

diffX1_X2_2 is continuous by Th61, JORDAN5A:27;

coherence

Proj2_1 is continuous by Th62, JORDAN5A:27;

coherence

Proj2_2 is continuous by Th63, JORDAN5A:27;

definition

let n be non zero Element of NAT ;

let o, p be Point of (TOP-REAL n);

let r be positive Real;

assume A1: p is Point of (Tdisk (o,r)) ;

set X = (TOP-REAL n) | ((cl_Ball (o,r)) \ {p});

ex b_{1} 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 & b_{1} . x = HC (p,y,o,r) )

for b_{1}, b_{2} 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 & b_{1} . x = HC (p,y,o,r) ) ) & ( for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st

( x = y & b_{2} . x = HC (p,y,o,r) ) ) holds

b_{1} = b_{2}

end;
let o, p be Point of (TOP-REAL n);

let r be positive Real;

assume A1: p is Point of (Tdisk (o,r)) ;

set X = (TOP-REAL n) | ((cl_Ball (o,r)) \ {p});

func DiskProj (o,r,p) -> Function of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})),(Tcircle (o,r)) means :Def7: :: JORDAN:def 7

for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st

( x = y & it . x = HC (p,y,o,r) );

existence for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st

( x = y & it . x = HC (p,y,o,r) );

ex b

for x being Point of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) ex y being Point of (TOP-REAL n) st

( x = y & b

proof end;

uniqueness for b

( x = y & b

( x = y & b

b

proof end;

:: deftheorem Def7 defines DiskProj JORDAN:def 7 :

for n being non zero Element of NAT

for o, p being Point of (TOP-REAL n)

for r being positive Real st p is Point of (Tdisk (o,r)) holds

for b_{5} being Function of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})),(Tcircle (o,r)) holds

( b_{5} = 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 & b_{5} . x = HC (p,y,o,r) ) );

for n being non zero Element of NAT

for o, p being Point of (TOP-REAL n)

for r being positive Real st p is Point of (Tdisk (o,r)) holds

for b

( b

( x = y & b

theorem Th64: :: JORDAN:64

for o, p being Point of (TOP-REAL 2)

for r being positive Real st p is Point of (Tdisk (o,r)) holds

DiskProj (o,r,p) is continuous

for r being positive Real st p is Point of (Tdisk (o,r)) holds

DiskProj (o,r,p) is continuous

proof end;

theorem Th65: :: JORDAN:65

for n being non zero Element of NAT

for o, p being Point of (TOP-REAL n)

for r being positive Real st p in Ball (o,r) holds

(DiskProj (o,r,p)) | (Sphere (o,r)) = id (Sphere (o,r))

for o, p being Point of (TOP-REAL n)

for r being positive Real st p in Ball (o,r) holds

(DiskProj (o,r,p)) | (Sphere (o,r)) = id (Sphere (o,r))

proof end;

definition

let n be non zero Element of NAT ;

let o, p be Point of (TOP-REAL n);

let r be positive Real;

assume A1: p in Ball (o,r) ;

set X = Tcircle (o,r);

ex b_{1} 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 & b_{1} . x = HC (y,p,o,r) )

for b_{1}, b_{2} 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 & b_{1} . x = HC (y,p,o,r) ) ) & ( for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st

( x = y & b_{2} . x = HC (y,p,o,r) ) ) holds

b_{1} = b_{2}

end;
let o, p be Point of (TOP-REAL n);

let r be positive Real;

assume A1: p in Ball (o,r) ;

set X = Tcircle (o,r);

func RotateCircle (o,r,p) -> Function of (Tcircle (o,r)),(Tcircle (o,r)) means :Def8: :: JORDAN:def 8

for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st

( x = y & it . x = HC (y,p,o,r) );

existence for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st

( x = y & it . x = HC (y,p,o,r) );

ex b

for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st

( x = y & b

proof end;

uniqueness for b

( x = y & b

( x = y & b

b

proof end;

:: deftheorem Def8 defines RotateCircle JORDAN:def 8 :

for n being non zero Element of NAT

for o, p being Point of (TOP-REAL n)

for r being positive Real st p in Ball (o,r) holds

for b_{5} being Function of (Tcircle (o,r)),(Tcircle (o,r)) holds

( b_{5} = RotateCircle (o,r,p) iff for x being Point of (Tcircle (o,r)) ex y being Point of (TOP-REAL n) st

( x = y & b_{5} . x = HC (y,p,o,r) ) );

for n being non zero Element of NAT

for o, p being Point of (TOP-REAL n)

for r being positive Real st p in Ball (o,r) holds

for b

( b

( x = y & b

theorem Th66: :: JORDAN:66

for o, p being Point of (TOP-REAL 2)

for r being positive Real st p in Ball (o,r) holds

RotateCircle (o,r,p) is continuous

for r being positive Real st p in Ball (o,r) holds

RotateCircle (o,r,p) is continuous

proof end;

theorem Th67: :: JORDAN:67

for n being non zero Element of NAT

for o, p being Point of (TOP-REAL n)

for r being positive Real st p in Ball (o,r) holds

RotateCircle (o,r,p) is without_fixpoints

for o, p being Point of (TOP-REAL n)

for r being positive Real st p in Ball (o,r) holds

RotateCircle (o,r,p) is without_fixpoints

proof end;

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 & U is a_component & V is a_component & U <> V holds

Cl P misses V

for P being Subset of (TOP-REAL 2)

for U, V being Subset of ((TOP-REAL 2) | (C `)) st U = P & U is a_component & V is a_component & U <> V holds

Cl P misses V

proof end;

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

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

((TOP-REAL 2) | (C `)) | U is pathwise_connected

proof end;

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

for A being Subset of (TOP-REAL 2)

for r being non negative Real st A is_an_arc_of p1,p2 & A is Subset of (Tdisk (p,r)) holds

ex f being Function of (Tdisk (p,r)),((TOP-REAL 2) | A) st

( f is continuous & f | A = id A )

proof end;

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

for C being Simple_closed_curve

for A, B, P being Subset of (TOP-REAL 2)

for U being Subset of ((TOP-REAL 2) | (C `))

for r being positive Real st A is_an_arc_of p1,p2 & A c= C & C c= Ball (p,r) & p in U & (Cl P) /\ (P `) c= A & P c= Ball (p,r) holds

for f being Function of (Tdisk (p,r)),((TOP-REAL 2) | A) st f is continuous & f | A = id A & U = P & U is a_component & B = (cl_Ball (p,r)) \ {p} holds

ex g being Function of (Tdisk (p,r)),((TOP-REAL 2) | B) st

( g is continuous & ( for x being Point of (Tdisk (p,r)) holds

( ( x in Cl P implies g . x = f . x ) & ( x in P ` implies g . x = x ) ) ) )

proof end;

Lm14: for p being Point of (TOP-REAL 2)

for C being Simple_closed_curve

for B, P 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 st A c= C & C c= Ball (p,r) & p in V & (Cl P) /\ (P `) c= A & Ball (p,r) meets P holds

for f being Function of (Tdisk (p,r)),((TOP-REAL 2) | A) st f is continuous & f | A = id A & U = P & U is a_component & V is a_component & B = (cl_Ball (p,r)) \ {p} holds

ex g being Function of (Tdisk (p,r)),((TOP-REAL 2) | B) st

( g is continuous & ( for x being Point of (Tdisk (p,r)) holds

( ( x in Cl P implies g . x = x ) & ( x in P ` implies g . x = f . x ) ) ) )

proof end;

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 & U = P & U is a_component holds

C = Fr P

proof end;

set rp = 1;

set rl = - 1;

set rg = 3;

set rd = - 3;

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

set b = |[1,0]|;

set c = |[0,3]|;

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

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

set pg = |[1,3]|;

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

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

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

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

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

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;

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;

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;

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;

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 & p `2 <= 3 & p `2 >= - 3 ) or ( p `1 <= 1 & p `1 >= - 1 & p `2 = 3 ) or ( p `1 <= 1 & p `1 >= - 1 & p `2 = - 3 ) or ( p `1 = 1 & p `2 <= 3 & p `2 >= - 3 ) ) }

by SPPOL_2: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

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

proof end;

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)

P c= closed_inside_of_rectangle ((- 1),1,(- 3),3)

proof end;

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;

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;

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;

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;

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

p in LSeg (|[1,3]|,|[1,0]|)

proof end;

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

p in LSeg (|[1,(- 3)]|,|[1,0]|)

proof end;

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

P misses LSeg (|[(- 1),3]|,|[1,3]|)

proof end;

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

P misses LSeg (|[(- 1),(- 3)]|,|[1,(- 3)]|)

proof end;

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

P /\ (rectangle ((- 1),1,(- 3),3)) = {|[(- 1),0]|,|[1,0]|}

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 & p in C ` & p in LSeg (|[(- 1),0]|,|[(- 1),3]|) holds

LSeg (p,|[(- 1),3]|) misses C

proof end;

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 & p in C ` & p in LSeg (|[1,0]|,|[1,3]|) holds

LSeg (p,|[1,3]|) misses C

proof end;

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 & p in C ` & p in LSeg (|[(- 1),0]|,|[(- 1),(- 3)]|) holds

LSeg (p,|[(- 1),(- 3)]|) misses C

proof end;

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 & p in C ` & p in LSeg (|[1,0]|,|[1,(- 3)]|) holds

LSeg (p,|[1,(- 3)]|) misses C

proof end;

Lm86: for r being Real holds

( not |[0,r]| in rectangle ((- 1),1,(- 3),3) or r = - 3 or r = 3 )

proof end;

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

W-bound P = - 1

proof end;

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

W-most P = {|[(- 1),0]|}

proof end;

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

E-most P = {|[1,0]|}

proof end;

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]| & W-max P = |[(- 1),0]| )

( W-min P = |[(- 1),0]| & W-max P = |[(- 1),0]| )

proof end;

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]| & E-max P = |[1,0]| )

( E-min P = |[1,0]| & E-max P = |[1,0]| )

proof end;

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

proof end;

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

proof end;

theorem Th81: :: JORDAN:81

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

LSeg (|[0,3]|,(UMP P)) is vertical

LSeg (|[0,3]|,(UMP P)) is vertical

proof end;

theorem Th82: :: JORDAN:82

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

LSeg ((LMP P),|[0,(- 3)]|) is vertical

LSeg ((LMP P),|[0,(- 3)]|) is vertical

proof end;

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 & p in P holds

p `2 < 3

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

p `2 < 3

proof end;

theorem 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 & p in P holds

- 3 < p `2

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

- 3 < p `2

proof end;

theorem 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 & p in LSeg (|[0,3]|,(UMP D)) holds

(UMP D) `2 <= p `2

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

(UMP D) `2 <= p `2

proof end;

theorem 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 & p in LSeg ((LMP D),|[0,(- 3)]|) holds

p `2 <= (LMP D) `2

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

p `2 <= (LMP D) `2

proof end;

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

LSeg (|[0,3]|,(UMP D)) c= north_halfline (UMP D)

proof end;

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)

LSeg ((LMP D),|[0,(- 3)]|) c= south_halfline (LMP D)

proof end;

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 & P is_inside_component_of C holds

LSeg (|[0,3]|,(UMP C)) misses P

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

LSeg (|[0,3]|,(UMP C)) misses P

proof end;

theorem 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 & P is_inside_component_of C holds

LSeg ((LMP C),|[0,(- 3)]|) misses P

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

LSeg ((LMP C),|[0,(- 3)]|) misses P

proof end;

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

(LSeg (|[0,3]|,(UMP D))) /\ D = {(UMP D)}

proof end;

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

(LSeg (|[0,(- 3)]|,(LMP D))) /\ D = {(LMP D)}

proof end;

theorem Th93: :: JORDAN:93

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

A c= closed_inside_of_rectangle ((- 1),1,(- 3),3)

A c= closed_inside_of_rectangle ((- 1),1,(- 3),3)

proof end;

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)

proof end;

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

LSeg (|[0,3]|,|[0,(- 3)]|) meets C

proof end;

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

proof end;

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

for Ux being Subset of (TOP-REAL 2) st Ux = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) holds

( Ux is_inside_component_of C & ( for V being Subset of (TOP-REAL 2) st V is_inside_component_of C holds

V = Ux ) )

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

for Ux being Subset of (TOP-REAL 2) st Ux = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `))) holds

( Ux is_inside_component_of C & ( for V being Subset of (TOP-REAL 2) st V is_inside_component_of C holds

V = Ux ) )

proof end;

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

BDD C = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `)))

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

BDD C = Component_of (Down (((1 / 2) * ((UMP ((LSeg ((LMP Jc),|[0,(- 3)]|)) /\ Jd)) + (LMP Jc))),(C `)))

proof end;

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

C is Jordan

proof end;

Lm92: for C being Simple_closed_curve holds C is Jordan

proof end;

registration
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 & U is a_component holds

C = Fr P

for P being Subset of (TOP-REAL 2)

for U being Subset of ((TOP-REAL 2) | (C `)) st U = P & U is a_component holds

C = Fr P

proof end;

theorem :: JORDAN:98

for C being Simple_closed_curve ex A1, A2 being Subset of (TOP-REAL 2) st

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

( C1 is a_component & C2 is a_component ) ) )

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

( C1 is a_component & C2 is a_component ) ) )

proof end;

:: Jordan Curve Theorem