:: by Yatsuka Nakamura and Andrzej Trybulec

::

:: Received December 19, 1997

:: Copyright (c) 1997-2012 Association of Mizar Users

begin

theorem Th2: :: JORDAN6:2

for TX being non empty TopSpace

for P being Subset of TX

for A being Subset of (TX | P)

for B being Subset of TX st B is closed & A = B /\ P holds

A is closed

for P being Subset of TX

for A being Subset of (TX | P)

for B being Subset of TX st B is closed & A = B /\ P holds

A is closed

proof end;

theorem Th3: :: JORDAN6:3

for TX, TY being non empty TopSpace

for P being non empty Subset of TY

for f being Function of TX,(TY | P) holds

( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds

f2 is continuous ) )

for P being non empty Subset of TY

for f being Function of TX,(TY | P) holds

( f is Function of TX,TY & ( for f2 being Function of TX,TY st f2 = f & f is continuous holds

f2 is continuous ) )

proof end;

theorem Th4: :: JORDAN6:4

for r being real number

for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 >= r } holds

P is closed

for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 >= r } holds

P is closed

proof end;

theorem Th5: :: JORDAN6:5

for r being real number

for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 <= r } holds

P is closed

for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 <= r } holds

P is closed

proof end;

theorem Th6: :: JORDAN6:6

for r being real number

for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 = r } holds

P is closed

for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `1 = r } holds

P is closed

proof end;

theorem Th7: :: JORDAN6:7

for r being real number

for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 >= r } holds

P is closed

for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 >= r } holds

P is closed

proof end;

theorem Th8: :: JORDAN6:8

for r being real number

for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 <= r } holds

P is closed

for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 <= r } holds

P is closed

proof end;

theorem Th9: :: JORDAN6:9

for r being real number

for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 = r } holds

P is closed

for P being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : p `2 = r } holds

P is closed

proof end;

theorem Th10: :: JORDAN6:10

for n being Element of NAT

for P being Subset of (TOP-REAL n)

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

P is connected

for P being Subset of (TOP-REAL n)

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

P is connected

proof end;

theorem :: JORDAN6:11

for P being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

P is closed by COMPTS_1:7, JORDAN5A:1;

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

P is closed by COMPTS_1:7, JORDAN5A:1;

theorem Th12: :: JORDAN6:12

for P being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

ex q being Point of (TOP-REAL 2) st

( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 )

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

ex q being Point of (TOP-REAL 2) st

( q in P & q `1 = ((p1 `1) + (p2 `1)) / 2 )

proof end;

theorem Th13: :: JORDAN6:13

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

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds

( P meets Q & P /\ Q is closed )

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds

( P meets Q & P /\ Q is closed )

proof end;

theorem Th14: :: JORDAN6:14

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

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds

( P meets Q & P /\ Q is closed )

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds

( P meets Q & P /\ Q is closed )

proof end;

definition

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

let p1, p2 be Point of (TOP-REAL 2);

ex b_{1} being Point of (TOP-REAL 2) st

for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds

b_{1} = First_Point (P,p1,p2,Q)

for b_{1}, b_{2} being Point of (TOP-REAL 2) st ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds

b_{1} = First_Point (P,p1,p2,Q) ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds

b_{2} = First_Point (P,p1,p2,Q) ) holds

b_{1} = b_{2}

end;
let p1, p2 be Point of (TOP-REAL 2);

func x_Middle (P,p1,p2) -> Point of (TOP-REAL 2) means :Def1: :: JORDAN6:def 1

for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds

it = First_Point (P,p1,p2,Q);

existence for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds

it = First_Point (P,p1,p2,Q);

ex b

for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines x_Middle JORDAN6:def 1 :

for P being Subset of (TOP-REAL 2)

for p1, p2, b_{4} being Point of (TOP-REAL 2) holds

( b_{4} = x_Middle (P,p1,p2) iff for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2 } holds

b_{4} = First_Point (P,p1,p2,Q) );

for P being Subset of (TOP-REAL 2)

for p1, p2, b

( b

b

definition

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

let p1, p2 be Point of (TOP-REAL 2);

ex b_{1} being Point of (TOP-REAL 2) st

for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds

b_{1} = First_Point (P,p1,p2,Q)

for b_{1}, b_{2} being Point of (TOP-REAL 2) st ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds

b_{1} = First_Point (P,p1,p2,Q) ) & ( for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds

b_{2} = First_Point (P,p1,p2,Q) ) holds

b_{1} = b_{2}

end;
let p1, p2 be Point of (TOP-REAL 2);

func y_Middle (P,p1,p2) -> Point of (TOP-REAL 2) means :Def2: :: JORDAN6:def 2

for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds

it = First_Point (P,p1,p2,Q);

existence for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds

it = First_Point (P,p1,p2,Q);

ex b

for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines y_Middle JORDAN6:def 2 :

for P being Subset of (TOP-REAL 2)

for p1, p2, b_{4} being Point of (TOP-REAL 2) holds

( b_{4} = y_Middle (P,p1,p2) iff for Q being Subset of (TOP-REAL 2) st Q = { q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2 } holds

b_{4} = First_Point (P,p1,p2,Q) );

for P being Subset of (TOP-REAL 2)

for p1, p2, b

( b

b

theorem :: JORDAN6:15

for P being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P )

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

( x_Middle (P,p1,p2) in P & y_Middle (P,p1,p2) in P )

proof end;

theorem :: JORDAN6:16

for P being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 )

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

( p1 = x_Middle (P,p1,p2) iff p1 `1 = p2 `1 )

proof end;

theorem :: JORDAN6:17

for P being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 )

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

( p1 = y_Middle (P,p1,p2) iff p1 `2 = p2 `2 )

proof end;

begin

theorem Th18: :: JORDAN6:18

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 & LE q1,q2,P,p1,p2 holds

LE q2,q1,P,p2,p1

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

LE q2,q1,P,p2,p1

proof end;

definition

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

let p1, p2, q1 be Point of (TOP-REAL 2);

{ q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } is Subset of (TOP-REAL 2)

end;
let p1, p2, q1 be Point of (TOP-REAL 2);

func L_Segment (P,p1,p2,q1) -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 3

{ q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } ;

coherence { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } ;

{ q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } is Subset of (TOP-REAL 2)

proof end;

:: deftheorem defines L_Segment JORDAN6:def 3 :

for P being Subset of (TOP-REAL 2)

for p1, p2, q1 being Point of (TOP-REAL 2) holds L_Segment (P,p1,p2,q1) = { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } ;

for P being Subset of (TOP-REAL 2)

for p1, p2, q1 being Point of (TOP-REAL 2) holds L_Segment (P,p1,p2,q1) = { q where q is Point of (TOP-REAL 2) : LE q,q1,P,p1,p2 } ;

definition

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

let p1, p2, q1 be Point of (TOP-REAL 2);

{ q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } is Subset of (TOP-REAL 2)

end;
let p1, p2, q1 be Point of (TOP-REAL 2);

func R_Segment (P,p1,p2,q1) -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 4

{ q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ;

coherence { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ;

{ q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } is Subset of (TOP-REAL 2)

proof end;

:: deftheorem defines R_Segment JORDAN6:def 4 :

for P being Subset of (TOP-REAL 2)

for p1, p2, q1 being Point of (TOP-REAL 2) holds R_Segment (P,p1,p2,q1) = { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ;

for P being Subset of (TOP-REAL 2)

for p1, p2, q1 being Point of (TOP-REAL 2) holds R_Segment (P,p1,p2,q1) = { q where q is Point of (TOP-REAL 2) : LE q1,q,P,p1,p2 } ;

theorem Th19: :: JORDAN6:19

for P being Subset of (TOP-REAL 2)

for p1, p2, q1 being Point of (TOP-REAL 2) holds L_Segment (P,p1,p2,q1) c= P

for p1, p2, q1 being Point of (TOP-REAL 2) holds L_Segment (P,p1,p2,q1) c= P

proof end;

theorem Th20: :: JORDAN6:20

for P being Subset of (TOP-REAL 2)

for p1, p2, q1 being Point of (TOP-REAL 2) holds R_Segment (P,p1,p2,q1) c= P

for p1, p2, q1 being Point of (TOP-REAL 2) holds R_Segment (P,p1,p2,q1) c= P

proof end;

theorem :: JORDAN6:21

for P being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

L_Segment (P,p1,p2,p1) = {p1}

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

L_Segment (P,p1,p2,p1) = {p1}

proof end;

theorem :: JORDAN6:22

for P being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

L_Segment (P,p1,p2,p2) = P

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

L_Segment (P,p1,p2,p2) = P

proof end;

theorem :: JORDAN6:23

for P being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

R_Segment (P,p1,p2,p2) = {p2}

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

R_Segment (P,p1,p2,p2) = {p2}

proof end;

theorem :: JORDAN6:24

for P being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

R_Segment (P,p1,p2,p1) = P

for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

R_Segment (P,p1,p2,p1) = P

proof end;

theorem :: JORDAN6:25

for P being Subset of (TOP-REAL 2)

for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1)

for p1, p2, q1 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

R_Segment (P,p1,p2,q1) = L_Segment (P,p2,p1,q1)

proof end;

definition

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

let p1, p2, q1, q2 be Point of (TOP-REAL 2);

coherence

(R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2)) is Subset of (TOP-REAL 2);

;

end;
let p1, p2, q1, q2 be Point of (TOP-REAL 2);

func Segment (P,p1,p2,q1,q2) -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 5

(R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2));

correctness (R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2));

coherence

(R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2)) is Subset of (TOP-REAL 2);

;

:: deftheorem defines Segment JORDAN6:def 5 :

for P being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (P,p1,p2,q1,q2) = (R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2));

for P being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (P,p1,p2,q1,q2) = (R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2));

theorem :: JORDAN6:26

for P being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (P,p1,p2,q1,q2) = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }

for p1, p2, q1, q2 being Point of (TOP-REAL 2) holds Segment (P,p1,p2,q1,q2) = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,P,p1,p2 & LE q,q2,P,p1,p2 ) }

proof end;

theorem :: JORDAN6:27

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 & LE q2,q1,P,p2,p1 holds

LE q1,q2,P,p1,p2 by Th18, JORDAN5B:14;

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

LE q1,q2,P,p1,p2 by Th18, JORDAN5B:14;

theorem Th28: :: JORDAN6:28

for P being Subset of (TOP-REAL 2)

for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

L_Segment (P,p1,p2,q) = R_Segment (P,p2,p1,q)

for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 holds

L_Segment (P,p1,p2,q) = R_Segment (P,p2,p1,q)

proof end;

theorem :: JORDAN6:29

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 holds

Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1)

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

Segment (P,p1,p2,q1,q2) = Segment (P,p2,p1,q2,q1)

proof end;

begin

definition

let s be real number ;

coherence

{ p where p is Point of (TOP-REAL 2) : p `1 = s } is Subset of (TOP-REAL 2);

coherence

{ p where p is Point of (TOP-REAL 2) : p `2 = s } is Subset of (TOP-REAL 2);

end;
func Vertical_Line s -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 6

{ p where p is Point of (TOP-REAL 2) : p `1 = s } ;

correctness { p where p is Point of (TOP-REAL 2) : p `1 = s } ;

coherence

{ p where p is Point of (TOP-REAL 2) : p `1 = s } is Subset of (TOP-REAL 2);

proof end;

func Horizontal_Line s -> Subset of (TOP-REAL 2) equals :: JORDAN6:def 7

{ p where p is Point of (TOP-REAL 2) : p `2 = s } ;

correctness { p where p is Point of (TOP-REAL 2) : p `2 = s } ;

coherence

{ p where p is Point of (TOP-REAL 2) : p `2 = s } is Subset of (TOP-REAL 2);

proof end;

:: deftheorem defines Vertical_Line JORDAN6:def 6 :

for s being real number holds Vertical_Line s = { p where p is Point of (TOP-REAL 2) : p `1 = s } ;

for s being real number holds Vertical_Line s = { p where p is Point of (TOP-REAL 2) : p `1 = s } ;

:: deftheorem defines Horizontal_Line JORDAN6:def 7 :

for s being real number holds Horizontal_Line s = { p where p is Point of (TOP-REAL 2) : p `2 = s } ;

for s being real number holds Horizontal_Line s = { p where p is Point of (TOP-REAL 2) : p `2 = s } ;

theorem :: JORDAN6:30

for r being real number holds

( Vertical_Line r is closed & Horizontal_Line r is closed ) by Th6, Th9;

( Vertical_Line r is closed & Horizontal_Line r is closed ) by Th6, Th9;

theorem Th31: :: JORDAN6:31

for r being real number

for p being Point of (TOP-REAL 2) holds

( p in Vertical_Line r iff p `1 = r )

for p being Point of (TOP-REAL 2) holds

( p in Vertical_Line r iff p `1 = r )

proof end;

theorem :: JORDAN6:32

for r being real number

for p being Point of (TOP-REAL 2) holds

( p in Horizontal_Line r iff p `2 = r )

for p being Point of (TOP-REAL 2) holds

( p in Horizontal_Line r iff p `2 = r )

proof end;

theorem Th33: :: JORDAN6:33

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

ex P1, P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

ex P1, P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

proof end;

begin

theorem Th36: :: JORDAN6:36

for P7 being Subset of I[01] st P7 = the carrier of I[01] \ {0,1} holds

( P7 <> {} & P7 is connected )

( P7 <> {} & P7 is connected )

proof end;

theorem Th37: :: JORDAN6:37

for n being Element of NAT

for P being Subset of (TOP-REAL n)

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

p1 <> p2

for P being Subset of (TOP-REAL n)

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

p1 <> p2

proof end;

theorem :: JORDAN6:38

for n being Element of NAT

for P being Subset of (TOP-REAL n)

for Q being Subset of ((TOP-REAL n) | P)

for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds

Q is open

for P being Subset of (TOP-REAL n)

for Q being Subset of ((TOP-REAL n) | P)

for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds

Q is open

proof end;

::A proof of the following is almost same as JORDAN5A:1.

theorem Th39: :: JORDAN6:39

for n being Element of NAT

for P, P1, P2 being Subset of (TOP-REAL n)

for Q being Subset of ((TOP-REAL n) | P)

for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds

Q is open

for P, P1, P2 being Subset of (TOP-REAL n)

for Q being Subset of ((TOP-REAL n) | P)

for p1, p2 being Point of (TOP-REAL n) st P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P1 /\ P2 = {p1,p2} & Q = P1 \ {p1,p2} holds

Q is open

proof end;

theorem Th40: :: JORDAN6:40

for n being Element of NAT

for P being Subset of (TOP-REAL n)

for Q being Subset of ((TOP-REAL n) | P)

for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds

Q is connected

for P being Subset of (TOP-REAL n)

for Q being Subset of ((TOP-REAL n) | P)

for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 & Q = P \ {p1,p2} holds

Q is connected

proof end;

theorem Th41: :: JORDAN6:41

for GX being TopSpace

for P1, P being Subset of GX

for Q9 being Subset of (GX | P1)

for Q being Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds

Q is connected

for P1, P being Subset of GX

for Q9 being Subset of (GX | P1)

for Q being Subset of (GX | P) st P1 c= P & Q = Q9 & Q9 is connected holds

Q is connected

proof end;

theorem Th42: :: JORDAN6:42

for n being Element of NAT

for P being Subset of (TOP-REAL n)

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

ex p3 being Point of (TOP-REAL n) st

( p3 in P & p3 <> p1 & p3 <> p2 )

for P being Subset of (TOP-REAL n)

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

ex p3 being Point of (TOP-REAL n) st

( p3 in P & p3 <> p1 & p3 <> p2 )

proof end;

theorem :: JORDAN6:43

for n being Element of NAT

for P being Subset of (TOP-REAL n)

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

P \ {p1,p2} <> {}

for P being Subset of (TOP-REAL n)

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

P \ {p1,p2} <> {}

proof end;

theorem :: JORDAN6:44

for n being Element of NAT

for P1, P being Subset of (TOP-REAL n)

for Q being Subset of ((TOP-REAL n) | P)

for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P1 c= P & Q = P1 \ {p1,p2} holds

Q is connected

for P1, P being Subset of (TOP-REAL n)

for Q being Subset of ((TOP-REAL n) | P)

for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P1 c= P & Q = P1 \ {p1,p2} holds

Q is connected

proof end;

theorem Th45: :: JORDAN6:45

for T, S, V being non empty TopSpace

for P1 being non empty Subset of S

for P2 being Subset of S

for f being Function of T,(S | P1)

for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds

ex h being Function of T,V st

( h = g * f & h is continuous )

for P1 being non empty Subset of S

for P2 being Subset of S

for f being Function of T,(S | P1)

for g being Function of (S | P2),V st P1 c= P2 & f is continuous & g is continuous holds

ex h being Function of T,V st

( h = g * f & h is continuous )

proof end;

theorem Th46: :: JORDAN6:46

for n being Element of NAT

for P1, P2 being Subset of (TOP-REAL n)

for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds

P1 = P2

for P1, P2 being Subset of (TOP-REAL n)

for p1, p2 being Point of (TOP-REAL n) st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 c= P2 holds

P1 = P2

proof end;

theorem Th47: :: JORDAN6:47

for P being Subset of (TOP-REAL 2)

for Q being Subset of ((TOP-REAL 2) | P)

for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} holds

not Q is connected

for Q being Subset of ((TOP-REAL 2) | P)

for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & p1 in P & p2 in P & p1 <> p2 & Q = P \ {p1,p2} holds

not Q is connected

proof end;

theorem Th48: :: JORDAN6:48

for P, P1, P2, P19, P29 being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P19 is_an_arc_of p1,p2 & P29 is_an_arc_of p1,p2 & P19 \/ P29 = P & not ( P1 = P19 & P2 = P29 ) holds

( P1 = P29 & P2 = P19 )

for p1, p2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = P & P19 is_an_arc_of p1,p2 & P29 is_an_arc_of p1,p2 & P19 \/ P29 = P & not ( P1 = P19 & P2 = P29 ) holds

( P1 = P29 & P2 = P19 )

proof end;

begin

Lm1: for g being Function of I[01],R^1

for s1, s2, r being real number st g is continuous & g . 0[01] < r & r < g . 1[01] holds

ex r1 being Real st

( 0 < r1 & r1 < 1 & g . r1 = r )

proof end;

theorem Th49: :: JORDAN6:49

for P1 being Subset of (TOP-REAL 2)

for r being real number

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

( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed )

for r being real number

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

( P1 meets Vertical_Line r & P1 /\ (Vertical_Line r) is closed )

proof end;

Lm2: now :: thesis: for P being Simple_closed_curve

for P1, P19 being non empty Subset of (TOP-REAL 2) st ex P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) & ex P29 being non empty Subset of (TOP-REAL 2) st

( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) holds

P1 = P19

for P1, P19 being non empty Subset of (TOP-REAL 2) st ex P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) & ex P29 being non empty Subset of (TOP-REAL 2) st

( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) holds

P1 = P19

let P be Simple_closed_curve; :: thesis: for P1, P19 being non empty Subset of (TOP-REAL 2) st ex P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) & ex P29 being non empty Subset of (TOP-REAL 2) st

( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) holds

P1 = P19

let P1, P19 be non empty Subset of (TOP-REAL 2); :: thesis: ( ex P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) & ex P29 being non empty Subset of (TOP-REAL 2) st

( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) implies P1 = P19 )

assume that

A1: ex P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) and

A2: ex P29 being non empty Subset of (TOP-REAL 2) st

( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ; :: thesis: P1 = P19

consider P2 being non empty Subset of (TOP-REAL 2) such that

A3: P1 is_an_arc_of W-min P, E-max P and

A4: P2 is_an_arc_of E-max P, W-min P and

P1 /\ P2 = {(W-min P),(E-max P)} and

A5: P1 \/ P2 = P and

A6: (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 by A1;

A7: P2 is_an_arc_of W-min P, E-max P by A4, JORDAN5B:14;

consider P29 being non empty Subset of (TOP-REAL 2) such that

A8: P19 is_an_arc_of W-min P, E-max P and

A9: P29 is_an_arc_of E-max P, W-min P and

P19 /\ P29 = {(W-min P),(E-max P)} and

A10: P19 \/ P29 = P and

A11: (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 by A2;

A12: P29 is_an_arc_of W-min P, E-max P by A9, JORDAN5B:14;

end;
( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) & ex P29 being non empty Subset of (TOP-REAL 2) st

( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) holds

P1 = P19

let P1, P19 be non empty Subset of (TOP-REAL 2); :: thesis: ( ex P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) & ex P29 being non empty Subset of (TOP-REAL 2) st

( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) implies P1 = P19 )

assume that

A1: ex P2 being non empty Subset of (TOP-REAL 2) st

( P1 is_an_arc_of W-min P, E-max P & P2 is_an_arc_of E-max P, W-min P & P1 /\ P2 = {(W-min P),(E-max P)} & P1 \/ P2 = P & (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) and

A2: ex P29 being non empty Subset of (TOP-REAL 2) st

( P19 is_an_arc_of W-min P, E-max P & P29 is_an_arc_of E-max P, W-min P & P19 /\ P29 = {(W-min P),(E-max P)} & P19 \/ P29 = P & (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ; :: thesis: P1 = P19

consider P2 being non empty Subset of (TOP-REAL 2) such that

A3: P1 is_an_arc_of W-min P, E-max P and

A4: P2 is_an_arc_of E-max P, W-min P and

P1 /\ P2 = {(W-min P),(E-max P)} and

A5: P1 \/ P2 = P and

A6: (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 by A1;

A7: P2 is_an_arc_of W-min P, E-max P by A4, JORDAN5B:14;

consider P29 being non empty Subset of (TOP-REAL 2) such that

A8: P19 is_an_arc_of W-min P, E-max P and

A9: P29 is_an_arc_of E-max P, W-min P and

P19 /\ P29 = {(W-min P),(E-max P)} and

A10: P19 \/ P29 = P and

A11: (First_Point (P19,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P29,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 by A2;

A12: P29 is_an_arc_of W-min P, E-max P by A9, JORDAN5B:14;

now :: thesis: ( P1 = P29 implies not P2 = P19 )

hence
P1 = P19
by A3, A5, A7, A8, A10, A12, Th48; :: thesis: verum
assume that

A13: P1 = P29 and

A14: P2 = P19 ; :: thesis: contradiction

A15: (W-min P) `1 = W-bound P by EUCLID:52;

A16: (E-max P) `1 = E-bound P by EUCLID:52;

then A17: (W-min P) `1 < (E-max P) `1 by A15, TOPREAL5:17;

then A18: (W-min P) `1 <= ((W-bound P) + (E-bound P)) / 2 by A15, A16, XREAL_1:226;

A19: ((W-bound P) + (E-bound P)) / 2 <= (E-max P) `1 by A15, A16, A17, XREAL_1:226;

then A20: P2 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A7, A18, Th49;

P2 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A7, A18, A19, Th49;

then A21: (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (First_Point (P2,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 by A4, A6, A20, JORDAN5C:18;

A22: P29 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A12, A18, A19, Th49;

P29 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A12, A18, A19, Th49;

hence contradiction by A9, A11, A13, A14, A21, A22, JORDAN5C:18; :: thesis: verum

end;
A13: P1 = P29 and

A14: P2 = P19 ; :: thesis: contradiction

A15: (W-min P) `1 = W-bound P by EUCLID:52;

A16: (E-max P) `1 = E-bound P by EUCLID:52;

then A17: (W-min P) `1 < (E-max P) `1 by A15, TOPREAL5:17;

then A18: (W-min P) `1 <= ((W-bound P) + (E-bound P)) / 2 by A15, A16, XREAL_1:226;

A19: ((W-bound P) + (E-bound P)) / 2 <= (E-max P) `1 by A15, A16, A17, XREAL_1:226;

then A20: P2 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A7, A18, Th49;

P2 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A7, A18, A19, Th49;

then A21: (First_Point (P1,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (First_Point (P2,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 by A4, A6, A20, JORDAN5C:18;

A22: P29 meets Vertical_Line (((W-bound P) + (E-bound P)) / 2) by A12, A18, A19, Th49;

P29 /\ (Vertical_Line (((W-bound P) + (E-bound P)) / 2)) is closed by A12, A18, A19, Th49;

hence contradiction by A9, A11, A13, A14, A21, A22, JORDAN5C:18; :: thesis: verum

definition

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

assume A1: P is being_simple_closed_curve ;

ex b_{1} being non empty Subset of (TOP-REAL 2) st

( b_{1} is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st

( P2 is_an_arc_of E-max P, W-min P & b_{1} /\ P2 = {(W-min P),(E-max P)} & b_{1} \/ P2 = P & (First_Point (b_{1},(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) )

for b_{1}, b_{2} being non empty Subset of (TOP-REAL 2) st b_{1} is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st

( P2 is_an_arc_of E-max P, W-min P & b_{1} /\ P2 = {(W-min P),(E-max P)} & b_{1} \/ P2 = P & (First_Point (b_{1},(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) & b_{2} is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st

( P2 is_an_arc_of E-max P, W-min P & b_{2} /\ P2 = {(W-min P),(E-max P)} & b_{2} \/ P2 = P & (First_Point (b_{2},(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) holds

b_{1} = b_{2}
by A1, Lm2;

end;
assume A1: P is being_simple_closed_curve ;

func Upper_Arc P -> non empty Subset of (TOP-REAL 2) means :Def8: :: JORDAN6:def 8

( it is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st

( P2 is_an_arc_of E-max P, W-min P & it /\ P2 = {(W-min P),(E-max P)} & it \/ P2 = P & (First_Point (it,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) );

existence ( it is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st

( P2 is_an_arc_of E-max P, W-min P & it /\ P2 = {(W-min P),(E-max P)} & it \/ P2 = P & (First_Point (it,(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) );

ex b

( b

( P2 is_an_arc_of E-max P, W-min P & b

proof end;

uniqueness for b

( P2 is_an_arc_of E-max P, W-min P & b

( P2 is_an_arc_of E-max P, W-min P & b

b

:: deftheorem Def8 defines Upper_Arc JORDAN6:def 8 :

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

for b_{2} being non empty Subset of (TOP-REAL 2) holds

( b_{2} = Upper_Arc P iff ( b_{2} is_an_arc_of W-min P, E-max P & ex P2 being non empty Subset of (TOP-REAL 2) st

( P2 is_an_arc_of E-max P, W-min P & b_{2} /\ P2 = {(W-min P),(E-max P)} & b_{2} \/ P2 = P & (First_Point (b_{2},(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) ) );

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

for b

( b

( P2 is_an_arc_of E-max P, W-min P & b

definition

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

assume A1: P is being_simple_closed_curve ;

then A2: Upper_Arc P is_an_arc_of W-min P, E-max P by Def8;

ex b_{1} being non empty Subset of (TOP-REAL 2) st

( b_{1} is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b_{1} = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b_{1} = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b_{1},(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
by A1, Def8;

uniqueness

for b_{1}, b_{2} being non empty Subset of (TOP-REAL 2) st b_{1} is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b_{1} = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b_{1} = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b_{1},(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 & b_{2} is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b_{2} = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b_{2} = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b_{2},(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 holds

b_{1} = b_{2}

end;
assume A1: P is being_simple_closed_curve ;

then A2: Upper_Arc P is_an_arc_of W-min P, E-max P by Def8;

func Lower_Arc P -> non empty Subset of (TOP-REAL 2) means :Def9: :: JORDAN6:def 9

( it is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ it = {(W-min P),(E-max P)} & (Upper_Arc P) \/ it = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (it,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 );

existence ( it is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ it = {(W-min P),(E-max P)} & (Upper_Arc P) \/ it = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (it,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 );

ex b

( b

uniqueness

for b

b

proof end;

:: deftheorem Def9 defines Lower_Arc JORDAN6:def 9 :

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

for b_{2} being non empty Subset of (TOP-REAL 2) holds

( b_{2} = Lower_Arc P iff ( b_{2} is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ b_{2} = {(W-min P),(E-max P)} & (Upper_Arc P) \/ b_{2} = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b_{2},(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) );

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

for b

( b

theorem Th50: :: JORDAN6:50

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

( Upper_Arc P is_an_arc_of W-min P, E-max P & Upper_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of W-min P, E-max P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

( Upper_Arc P is_an_arc_of W-min P, E-max P & Upper_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of E-max P, W-min P & Lower_Arc P is_an_arc_of W-min P, E-max P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )

proof end;

theorem Th51: :: JORDAN6:51

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

( Lower_Arc P = (P \ (Upper_Arc P)) \/ {(W-min P),(E-max P)} & Upper_Arc P = (P \ (Lower_Arc P)) \/ {(W-min P),(E-max P)} )

( Lower_Arc P = (P \ (Upper_Arc P)) \/ {(W-min P),(E-max P)} & Upper_Arc P = (P \ (Lower_Arc P)) \/ {(W-min P),(E-max P)} )

proof end;

theorem :: JORDAN6:52

for P being Subset of (TOP-REAL 2)

for P1 being Subset of ((TOP-REAL 2) | P) st P is being_simple_closed_curve & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P holds

P1 = Lower_Arc P

for P1 being Subset of ((TOP-REAL 2) | P) st P is being_simple_closed_curve & (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P1 = P holds

P1 = Lower_Arc P

proof end;

theorem :: JORDAN6:53

for P being Subset of (TOP-REAL 2)

for P1 being Subset of ((TOP-REAL 2) | P) st P is being_simple_closed_curve & P1 /\ (Lower_Arc P) = {(W-min P),(E-max P)} & P1 \/ (Lower_Arc P) = P holds

P1 = Upper_Arc P

for P1 being Subset of ((TOP-REAL 2) | P) st P is being_simple_closed_curve & P1 /\ (Lower_Arc P) = {(W-min P),(E-max P)} & P1 \/ (Lower_Arc P) = P holds

P1 = Upper_Arc P

proof end;

begin

theorem Th54: :: JORDAN6:54

for P being Subset of (TOP-REAL 2)

for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 holds

q = p1

for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE q,p1,P,p1,p2 holds

q = p1

proof end;

theorem Th55: :: JORDAN6:55

for P being Subset of (TOP-REAL 2)

for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2 holds

q = p2

for p1, p2, q being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & LE p2,q,P,p1,p2 holds

q = p2

proof end;

definition

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

let q1, q2 be Point of (TOP-REAL 2);

end;
let q1, q2 be Point of (TOP-REAL 2);

pred LE q1,q2,P means :Def10: :: JORDAN6:def 10

( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) );

( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) );

:: deftheorem Def10 defines LE JORDAN6:def 10 :

for P being Subset of (TOP-REAL 2)

for q1, q2 being Point of (TOP-REAL 2) holds

( LE q1,q2,P iff ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) );

for P being Subset of (TOP-REAL 2)

for q1, q2 being Point of (TOP-REAL 2) holds

( LE q1,q2,P iff ( ( q1 in Upper_Arc P & q2 in Lower_Arc P & not q2 = W-min P ) or ( q1 in Upper_Arc P & q2 in Upper_Arc P & LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P & q2 in Lower_Arc P & not q2 = W-min P & LE q1,q2, Lower_Arc P, E-max P, W-min P ) ) );

theorem :: JORDAN6:56

for P being Subset of (TOP-REAL 2)

for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q in P holds

LE q,q,P

for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q in P holds

LE q,q,P

proof end;

theorem :: JORDAN6:57

for P being Subset of (TOP-REAL 2)

for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds

q1 = q2

for q1, q2 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q1,P holds

q1 = q2

proof end;

theorem :: JORDAN6:58

for P being Subset of (TOP-REAL 2)

for q1, q2, q3 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P holds

LE q1,q3,P

for q1, q2, q3 being Point of (TOP-REAL 2) st P is being_simple_closed_curve & LE q1,q2,P & LE q2,q3,P holds

LE q1,q3,P

proof end;

theorem :: JORDAN6:59

for P being Subset of (TOP-REAL 2)

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

not p2 in L_Segment (P,p1,p2,q)

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

not p2 in L_Segment (P,p1,p2,q)

proof end;

theorem :: JORDAN6:60

for P being Subset of (TOP-REAL 2)

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

not p1 in R_Segment (P,p1,p2,q)

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

not p1 in R_Segment (P,p1,p2,q)

proof end;

registration

let S be non empty being_simple_closed_curve Subset of (TOP-REAL 2);

coherence

( not Lower_Arc S is empty & Lower_Arc S is compact )

( not Upper_Arc S is empty & Upper_Arc S is compact )

end;
coherence

( not Lower_Arc S is empty & Lower_Arc S is compact )

proof end;

coherence ( not Upper_Arc S is empty & Upper_Arc S is compact )

proof end;

theorem Th61: :: JORDAN6:61

for S being non empty being_simple_closed_curve Subset of (TOP-REAL 2) holds

( Lower_Arc S c= S & Upper_Arc S c= S )

( Lower_Arc S c= S & Upper_Arc S c= S )

proof end;

definition

let C be Simple_closed_curve;

First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is Point of (TOP-REAL 2) ;

First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is Point of (TOP-REAL 2) ;

end;
func Lower_Middle_Point C -> Point of (TOP-REAL 2) equals :: JORDAN6:def 11

First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));

coherence First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));

First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is Point of (TOP-REAL 2) ;

func Upper_Middle_Point C -> Point of (TOP-REAL 2) equals :: JORDAN6:def 12

First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));

coherence First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));

First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2))) is Point of (TOP-REAL 2) ;

:: deftheorem defines Lower_Middle_Point JORDAN6:def 11 :

for C being Simple_closed_curve holds Lower_Middle_Point C = First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));

for C being Simple_closed_curve holds Lower_Middle_Point C = First_Point ((Lower_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));

:: deftheorem defines Upper_Middle_Point JORDAN6:def 12 :

for C being Simple_closed_curve holds Upper_Middle_Point C = First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));

for C being Simple_closed_curve holds Upper_Middle_Point C = First_Point ((Upper_Arc C),(W-min C),(E-max C),(Vertical_Line (((W-bound C) + (E-bound C)) / 2)));

theorem Th62: :: JORDAN6:62

for C being Simple_closed_curve holds Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)

proof end;

theorem Th63: :: JORDAN6:63

for C being Simple_closed_curve holds Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)

proof end;

theorem :: JORDAN6:69

for C being Simple_closed_curve

for r being real number st W-bound C <= r & r <= E-bound C holds

LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_Arc C

for r being real number st W-bound C <= r & r <= E-bound C holds

LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_Arc C

proof end;

theorem :: JORDAN6:70

for C being Simple_closed_curve

for r being real number st W-bound C <= r & r <= E-bound C holds

LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C

for r being real number st W-bound C <= r & r <= E-bound C holds

LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C

proof end;