:: A Decomposition of Simple Closed Curves and an Order of Their Points
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received December 19, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

theorem Th1: :: JORDAN6:1
for r, s being real number st r <= s holds
( r <= (r + s) / 2 &amp; (r + s) / 2 <= s )
proofend;

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 &amp; A = B /\ P holds
A is closed
proofend;

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 &amp; ( for f2 being Function of TX,TY st f2 = f &amp; f is continuous holds
f2 is continuous ) )
proofend;

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

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

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

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

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

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

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

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;

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 &amp; q `1 = ((p1 `1) + (p2 `1)) / 2 )
proofend;

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 &amp; Q =  {  q where q is Point of (TOP-REAL 2) : q `1 = ((p1 `1) + (p2 `1)) / 2  }  holds
( P meets Q &amp; P /\ Q is closed )
proofend;

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 &amp; Q =  {  q where q is Point of (TOP-REAL 2) : q `2 = ((p1 `2) + (p2 `2)) / 2  }  holds
( P meets Q &amp; P /\ Q is closed )
proofend;

definition
let P be Subset of (TOP-REAL 2);
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
 ex b1 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
b1 = First_Point (P,p1,p2,Q)
proofend;
uniqueness
 for b1, b2 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
b1 = First_Point (P,p1,p2,Q) ) &amp; ( 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
b2 = First_Point (P,p1,p2,Q) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines x_Middle JORDAN6:def_1_:_
 for P being Subset of (TOP-REAL 2)
for p1, p2, b4 being Point of (TOP-REAL 2) holds
( b4 = 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
b4 = First_Point (P,p1,p2,Q) );

definition
let P be Subset of (TOP-REAL 2);
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
 ex b1 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
b1 = First_Point (P,p1,p2,Q)
proofend;
uniqueness
 for b1, b2 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
b1 = First_Point (P,p1,p2,Q) ) &amp; ( 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
b2 = First_Point (P,p1,p2,Q) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines y_Middle JORDAN6:def_2_:_
 for P being Subset of (TOP-REAL 2)
for p1, p2, b4 being Point of (TOP-REAL 2) holds
( b4 = 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
b4 = First_Point (P,p1,p2,Q) );

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 &amp; y_Middle (P,p1,p2) in P )
proofend;

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

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

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

definition
let P be Subset of (TOP-REAL 2);
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  }  is Subset of (TOP-REAL 2)
proofend;
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  }  ;

definition
let P be Subset of (TOP-REAL 2);
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  }  is Subset of (TOP-REAL 2)
proofend;
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  }  ;

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

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

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

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

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

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

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

definition
let P be Subset of (TOP-REAL 2);
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
coherence
(R_Segment (P,p1,p2,q1)) /\ (L_Segment (P,p1,p2,q2)) is Subset of (TOP-REAL 2);
;
end;

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

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 &amp; LE q,q2,P,p1,p2 )  }
proofend;

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 &amp; 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)
proofend;

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

begin

definition
let s be real number ;
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
coherence
{  p where p is Point of (TOP-REAL 2) : p `1 = s  }  is Subset of (TOP-REAL 2);
proofend;
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
coherence
{  p where p is Point of (TOP-REAL 2) : p `2 = s  }  is Subset of (TOP-REAL 2);
proofend;
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  }  ;

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

theorem :: JORDAN6:30
for r being real number holds
( Vertical_Line r is closed &amp; 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 )
proofend;

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

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 &amp; P2 is_an_arc_of E-max P, W-min P &amp; P1 /\ P2 = {(W-min P),(E-max P)} &amp; P1 \/ P2 = P &amp; (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 )
proofend;

begin

theorem Th34: :: JORDAN6:34
for P being Subset of I[01] st P = the carrier of I[01] \ {0,1} holds
P is open
proofend;

theorem :: JORDAN6:35
for P being Subset of R^1
for r, s being real number st P = ].r,s.[ holds
P is open
proofend;

theorem Th36: :: JORDAN6:36
for P7 being Subset of I[01] st P7 = the carrier of I[01] \ {0,1} holds
( P7 <> {} &amp; P7 is connected )
proofend;

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

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 &amp; Q = P \ {p1,p2} holds
Q is open
proofend;

::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 &amp; P1 \/ P2 = P &amp; P1 /\ P2 = {p1,p2} &amp; Q = P1 \ {p1,p2} holds
Q is open
proofend;

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 &amp; Q = P \ {p1,p2} holds
Q is connected
proofend;

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 &amp; Q = Q9 &amp; Q9 is connected holds
Q is connected
proofend;

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 &amp; p3 <> p1 &amp; p3 <> p2 )
proofend;

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

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 &amp; P1 c= P &amp; Q = P1 \ {p1,p2} holds
Q is connected
proofend;

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 &amp; f is continuous &amp; g is continuous holds
ex h being Function of T,V st
( h = g * f &amp; h is continuous )
proofend;

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 &amp; P2 is_an_arc_of p1,p2 &amp; P1 c= P2 holds
P1 = P2
proofend;

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 &amp; p1 in P &amp; p2 in P &amp; p1 <> p2 &amp; Q = P \ {p1,p2} holds
not Q is connected
proofend;

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 &amp; P1 is_an_arc_of p1,p2 &amp; P2 is_an_arc_of p1,p2 &amp; P1 \/ P2 = P &amp; P19 is_an_arc_of p1,p2 &amp; P29 is_an_arc_of p1,p2 &amp; P19 \/ P29 = P &amp; not ( P1 = P19 &amp; P2 = P29 ) holds
( P1 = P29 &amp; P2 = P19 )
proofend;

begin

Lm1:  for g being Function of I[01],R^1
for s1, s2, r being real number st g is continuous &amp; g . 0[01] < r &amp; r < g . 1[01] holds
ex r1 being Real st
( 0 < r1 &amp; r1 < 1 &amp; g . r1 = r )
proofend;

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 &amp; r <= p2 `1 &amp; P1 is_an_arc_of p1,p2 holds
( P1 meets Vertical_Line r &amp; P1 /\ (Vertical_Line r) is closed )
proofend;

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_&amp;_P2_is_an_arc_of_E-max_P,_W-min_P_&amp;_P1_/\_P2_=_{(W-min_P),(E-max_P)}_&amp;_P1_\/_P2_=_P_&amp;_(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_)_&amp;_ex_P29_being_non_empty_Subset_of_(TOP-REAL_2)_st_
(_P19_is_an_arc_of_W-min_P,_E-max_P_&amp;_P29_is_an_arc_of_E-max_P,_W-min_P_&amp;_P19_/\_P29_=_{(W-min_P),(E-max_P)}_&amp;_P19_\/_P29_=_P_&amp;_(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 &amp; P2 is_an_arc_of E-max P, W-min P &amp; P1 /\ P2 = {(W-min P),(E-max P)} &amp; P1 \/ P2 = P &amp; (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 ) &amp; ex P29 being non empty Subset of (TOP-REAL 2) st
( P19 is_an_arc_of W-min P, E-max P &amp; P29 is_an_arc_of E-max P, W-min P &amp; P19 /\ P29 = {(W-min P),(E-max P)} &amp; P19 \/ P29 = P &amp; (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 &amp; P2 is_an_arc_of E-max P, W-min P &amp; P1 /\ P2 = {(W-min P),(E-max P)} &amp; P1 \/ P2 = P &amp; (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 ) &amp; ex P29 being non empty Subset of (TOP-REAL 2) st
( P19 is_an_arc_of W-min P, E-max P &amp; P29 is_an_arc_of E-max P, W-min P &amp; P19 /\ P29 = {(W-min P),(E-max P)} &amp; P19 \/ P29 = P &amp; (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 &amp; P2 is_an_arc_of E-max P, W-min P &amp; P1 /\ P2 = {(W-min P),(E-max P)} &amp; P1 \/ P2 = P &amp; (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 &amp; P29 is_an_arc_of E-max P, W-min P &amp; P19 /\ P29 = {(W-min P),(E-max P)} &amp; P19 \/ P29 = P &amp; (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_)
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;
hence  P1 = P19 by A3, A5, A7, A8, A10, A12, Th48; ::_thesis: verum
end;

definition
let P be Subset of (TOP-REAL 2);
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 &amp; ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P &amp; it /\ P2 = {(W-min P),(E-max P)} &amp; it \/ P2 = P &amp; (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
 ex b1 being non empty Subset of (TOP-REAL 2) st
( b1 is_an_arc_of W-min P, E-max P &amp; ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P &amp; b1 /\ P2 = {(W-min P),(E-max P)} &amp; b1 \/ P2 = P &amp; (First_Point (b1,(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 ) )
proofend;
uniqueness
 for b1, b2 being non empty Subset of (TOP-REAL 2) st b1 is_an_arc_of W-min P, E-max P &amp; ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P &amp; b1 /\ P2 = {(W-min P),(E-max P)} &amp; b1 \/ P2 = P &amp; (First_Point (b1,(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 ) &amp; b2 is_an_arc_of W-min P, E-max P &amp; ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P &amp; b2 /\ P2 = {(W-min P),(E-max P)} &amp; b2 \/ P2 = P &amp; (First_Point (b2,(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
b1 = b2 by A1, Lm2;
end;

:: 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 b2 being non empty Subset of (TOP-REAL 2) holds
( b2 = Upper_Arc P iff ( b2 is_an_arc_of W-min P, E-max P &amp; ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P &amp; b2 /\ P2 = {(W-min P),(E-max P)} &amp; b2 \/ P2 = P &amp; (First_Point (b2,(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 ) ) );

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;
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 &amp; (Upper_Arc P) /\ it = {(W-min P),(E-max P)} &amp; (Upper_Arc P) \/ it = P &amp; (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
 ex b1 being non empty Subset of (TOP-REAL 2) st
( b1 is_an_arc_of E-max P, W-min P &amp; (Upper_Arc P) /\ b1 = {(W-min P),(E-max P)} &amp; (Upper_Arc P) \/ b1 = P &amp; (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) by A1, Def8;
uniqueness
 for b1, b2 being non empty Subset of (TOP-REAL 2) st b1 is_an_arc_of E-max P, W-min P &amp; (Upper_Arc P) /\ b1 = {(W-min P),(E-max P)} &amp; (Upper_Arc P) \/ b1 = P &amp; (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b1,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 &amp; b2 is_an_arc_of E-max P, W-min P &amp; (Upper_Arc P) /\ b2 = {(W-min P),(E-max P)} &amp; (Upper_Arc P) \/ b2 = P &amp; (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 holds
b1 = b2
proofend;
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 b2 being non empty Subset of (TOP-REAL 2) holds
( b2 = Lower_Arc P iff ( b2 is_an_arc_of E-max P, W-min P &amp; (Upper_Arc P) /\ b2 = {(W-min P),(E-max P)} &amp; (Upper_Arc P) \/ b2 = P &amp; (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (b2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 ) );

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 &amp; Upper_Arc P is_an_arc_of E-max P, W-min P &amp; Lower_Arc P is_an_arc_of E-max P, W-min P &amp; Lower_Arc P is_an_arc_of W-min P, E-max P &amp; (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} &amp; (Upper_Arc P) \/ (Lower_Arc P) = P &amp; (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 )
proofend;

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)} &amp; Upper_Arc P = (P \ (Lower_Arc P)) \/ {(W-min P),(E-max P)} )
proofend;

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 &amp; (Upper_Arc P) /\ P1 = {(W-min P),(E-max P)} &amp; (Upper_Arc P) \/ P1 = P holds
P1 = Lower_Arc P
proofend;

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 &amp; P1 /\ (Lower_Arc P) = {(W-min P),(E-max P)} &amp; P1 \/ (Lower_Arc P) = P holds
P1 = Upper_Arc P
proofend;

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 &amp; LE q,p1,P,p1,p2 holds
q = p1
proofend;

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 &amp; LE p2,q,P,p1,p2 holds
q = p2
proofend;

definition
let P be Subset of (TOP-REAL 2);
let q1, q2 be Point of (TOP-REAL 2);
pred LE q1,q2,P means :Def10: :: JORDAN6:def 10
( ( q1 in Upper_Arc P &amp; q2 in Lower_Arc P &amp; not q2 = W-min P ) or ( q1 in Upper_Arc P &amp; q2 in Upper_Arc P &amp; LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P &amp; q2 in Lower_Arc P &amp; not q2 = W-min P &amp; LE q1,q2, Lower_Arc P, E-max P, W-min P ) );
end;

:: 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 &amp; q2 in Lower_Arc P &amp; not q2 = W-min P ) or ( q1 in Upper_Arc P &amp; q2 in Upper_Arc P &amp; LE q1,q2, Upper_Arc P, W-min P, E-max P ) or ( q1 in Lower_Arc P &amp; q2 in Lower_Arc P &amp; not q2 = W-min P &amp; 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 &amp; q in P holds
LE q,q,P
proofend;

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 &amp; LE q1,q2,P &amp; LE q2,q1,P holds
q1 = q2
proofend;

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 &amp; LE q1,q2,P &amp; LE q2,q3,P holds
LE q1,q3,P
proofend;

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 &amp; q <> p2 holds
not p2 in L_Segment (P,p1,p2,q)
proofend;

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 &amp; q <> p1 holds
not p1 in R_Segment (P,p1,p2,q)
proofend;

registration
let S be non empty being_simple_closed_curve Subset of (TOP-REAL 2);
cluster Lower_Arc S ->  non empty compact ;
coherence
 ( not Lower_Arc S is empty &amp; Lower_Arc S is compact )
proofend;
cluster Upper_Arc S ->  non empty compact ;
coherence
 ( not Upper_Arc S is empty &amp; Upper_Arc S is compact )
proofend;
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 &amp; Upper_Arc S c= S )
proofend;

definition
let C be Simple_closed_curve;
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))) 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))) is Point of (TOP-REAL 2) ;
end;

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

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

theorem Th62: :: JORDAN6:62
for C being Simple_closed_curve holds Lower_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)
proofend;

theorem Th63: :: JORDAN6:63
for C being Simple_closed_curve holds Upper_Arc C meets Vertical_Line (((W-bound C) + (E-bound C)) / 2)
proofend;

theorem :: JORDAN6:64
for C being Simple_closed_curve holds (Lower_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2
proofend;

theorem :: JORDAN6:65
for C being Simple_closed_curve holds (Upper_Middle_Point C) `1 = ((W-bound C) + (E-bound C)) / 2
proofend;

theorem :: JORDAN6:66
for C being Simple_closed_curve holds Lower_Middle_Point C in Lower_Arc C
proofend;

theorem Th67: :: JORDAN6:67
for C being Simple_closed_curve holds Upper_Middle_Point C in Upper_Arc C
proofend;

theorem :: JORDAN6:68
for C being Simple_closed_curve holds Upper_Middle_Point C in C
proofend;

theorem :: JORDAN6:69
for C being Simple_closed_curve
for r being real number st W-bound C <= r &amp; r <= E-bound C holds
LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_Arc C
proofend;

theorem :: JORDAN6:70
for C being Simple_closed_curve
for r being real number st W-bound C <= r &amp; r <= E-bound C holds
LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C
proofend;