:: Jordan Curve Theorem
::  by Artur Korni{\l}owicz
::
:: Received September 15, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, TOPREAL2, RELAT_1, RCOMP_1,
      JORDAN21, TARSKI, XBOOLE_0, RELAT_2, METRIC_1, XXREAL_0, CARD_1, ARYTM_3,
      SUPINF_2, ARYTM_1, MCART_1, SPPOL_1, RLTOPSP1, PSCOMP_1, JORDAN6,
      JORDAN2C, CONVEX1, TOPREAL1, STRUCT_0, TOPMETR, VALUED_1, TREAL_1,
      ZFMISC_1, REAL_1, FUNCOP_1, ORDINAL2, COMPLEX1, BROUWER, TOPREALB,
      XCMPLX_0, TOPS_1, PCOMPS_1, XXREAL_2, FUNCT_1, TOPS_2, FUNCT_2, GRAPH_1,
      BORSUK_2, BORSUK_1, XXREAL_1, JGRAPH_6, JORDAN5C, JORDAN3, SQUARE_1,
      PARTFUN3, PARTFUN1, TOPREALA, SETFAM_1, PROB_1, ABIAN, CONNSP_1,
      CONNSP_2, TOPREAL4, FUNCT_4, TOPGRP_1, JORDAN24, CONNSP_3, JORDAN1,
      JORDAN, MEASURE5, SEQ_4, NAT_1, FUNCT_7;
 notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, SQUARE_1,
      MCART_1, RELAT_1, VALUED_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      FUNCT_3, FUNCT_4, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_2,
      XREAL_0, COMPLEX1, REAL_1, RCOMP_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1,
      BORSUK_1, TOPS_2, COMPTS_1, TREAL_1, CONNSP_1, CONNSP_2, CONNSP_3,
      METRIC_1, TBSP_1, RLVECT_1, PCOMPS_1, RLTOPSP1, EUCLID, BORSUK_2,
      TOPREAL1, TOPREAL2, TOPMETR, SPPOL_1, JORDAN1, JORDAN2C, JORDAN5C,
      TOPREAL4, JORDAN6, JGRAPH_6, TOPREAL6, TOPREAL9, BORSUK_6, TOPREALA,
      JORDAN21, TOPGRP_1, JORDAN24, ABIAN, PARTFUN3, TOPREALB, BROUWER,
      PSCOMP_1;
 constructors FUNCT_4, SQUARE_1, COMPLEX1, ABIAN, TOPS_1, CONNSP_1, COMPTS_1,
      TBSP_1, TSEP_1, TOPREAL1, TREAL_1, TOPREAL4, SPPOL_1, JORDAN1, SPPOL_2,
      CONNSP_3, WAYBEL_3, JORDAN5C, JORDAN6, TOPGRP_1, JORDAN2C, TOPREAL6,
      JORDAN21, JGRAPH_6, TOPREAL9, TOPREALA, PARTFUN3, BROUWER, JORDAN24,
      BORSUK_6, SEQ_4, FUNCSDOM, CONVEX1, BINOP_2, PSCOMP_1, XTUPLE_0, REAL_1;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS,
      XXREAL_0, XREAL_0, SQUARE_1, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, TOPS_1,
      COMPTS_1, METRIC_1, BORSUK_1, TEX_2, EUCLID, TOPMETR, TOPREAL1, TOPREAL2,
      SPPOL_1, JORDAN1, SPPOL_2, PSCOMP_1, BORSUK_2, WAYBEL_2, WAYBEL_3,
      JORDAN5A, JORDAN6, TOPGRP_1, YELLOW13, JORDAN2C, TOPREAL6, JORDAN21,
      TOPREAL9, TOPREALA, TOPREALB, RCOMP_3, PARTFUN3, TOPALG_5, BROUWER,
      JGRAPH_8, VALUED_0, XXREAL_2, RELAT_1, MEASURE6, PARTFUN4, VALUED_1,
      XTUPLE_0, ORDINAL1, CARD_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;


begin :: Preliminaries
:: I would like to thank Professor Yatsuka Nakamura
:: for including me to the team working on the formalization
:: of the Jordan Curve Theorem. Especially, I am very grateful
:: to Professor Nakamura for inviting me to Shinshu University, Nagano
:: to work on the project together.
:: I am also thankful to Professor Andrzej Trybulec for his
:: continual help and fruitful discussions during the formalization.

reserve a, b, c, d, r, s for Real,
  n for Element of NAT,
  p, p1, p2 for Point of TOP-REAL 2,
  x, y for Point of TOP-REAL n,
  C for Simple_closed_curve,
  A, B, P for Subset of TOP-REAL 2,
  U, V for Subset of (TOP-REAL 2)|C`,
  D for compact with_the_max_arc Subset of TOP-REAL 2;

registration
  let M be symmetric triangle Reflexive MetrStruct, x, y be Point of M;
  cluster dist(x,y) -> non negative;
end;

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

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

theorem :: JORDAN:2
  p1`2 < p2`2 implies p1`2 < (1/2*(p1+p2))`2;

theorem :: JORDAN:3
  p1`2 < p2`2 implies (1/2*(p1+p2))`2 < p2`2;

theorem :: JORDAN:4
  for A being vertical Subset of TOP-REAL 2 holds A /\ B is vertical;

theorem :: JORDAN:5
  for A being horizontal Subset of TOP-REAL 2 holds A /\ B is horizontal;

theorem :: JORDAN:6
  p in LSeg(p1,p2) & LSeg(p1,p2) is vertical implies LSeg(p,p2) is vertical;

theorem :: JORDAN:7
  p in LSeg(p1,p2) & LSeg(p1,p2) is horizontal implies LSeg(p,p2) is horizontal
;

registration

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

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

registration
  cluster vertical non empty compact -> with_the_max_arc for
Subset of TOP-REAL 2;
end;

theorem :: JORDAN:8
  p1`1 <= r & r <= p2`1 implies LSeg(p1,p2) meets Vertical_Line(r);

theorem :: JORDAN:9
  p1`2 <= r & r <= p2`2 implies LSeg(p1,p2) meets Horizontal_Line(r);

registration
  let n;
  cluster empty -> bounded for Subset of TOP-REAL n;
  cluster non bounded -> non empty for Subset of TOP-REAL n;
end;

registration
  let n be non zero Nat;
  cluster open closed non bounded convex for Subset of TOP-REAL n;
end;

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

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

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

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

theorem :: JORDAN:14
  A is_inside_component_of B implies UBD B misses A;

theorem :: JORDAN:15
  A is_outside_component_of B implies BDD B misses A;

theorem :: JORDAN:16
  for n being Nat
  for r being positive Real
  for a being Point of TOP-REAL n holds a in Ball(a,r);

theorem :: JORDAN:17
  for r being non negative Real
  for p being Point of TOP-REAL n holds p is Point of Tdisk(p,r);

registration
  let r be positive Real;
  let n be non zero Element of NAT;
  let p, q be Point of TOP-REAL n;
  cluster cl_Ball(p,r) \ {q} -> non empty;
end;

theorem :: JORDAN:18
  r <= s implies Ball(x,r) c= Ball(x,s);

theorem :: JORDAN:19
  cl_Ball(x,r) \ Ball(x,r) = Sphere(x,r);

theorem :: JORDAN:20
  y in Sphere(x,r) implies LSeg(x,y) \ {x,y} c= Ball(x,r);

theorem :: JORDAN:21
  r < s implies cl_Ball(x,r) c= Ball(x,s);

theorem :: JORDAN:22
  r < s implies Sphere(x,r) c= Ball(x,s);

theorem :: JORDAN:23
  for r being non zero Real holds Cl Ball(x,r) = cl_Ball(x,r);

theorem :: JORDAN:24
  for r being non zero Real holds Fr Ball(x,r) = Sphere(x,r);

registration
  let n be non zero Element of NAT;
  cluster bounded -> proper for Subset of TOP-REAL n;
end;

registration
  let n;
  cluster non empty closed convex bounded for Subset of TOP-REAL n;
  cluster non empty open convex bounded for Subset of TOP-REAL n;
end;

registration
  let n be Element of NAT;
  let A be bounded Subset of TOP-REAL n;
  cluster Cl A -> bounded;
end;

registration
  let n be Element of NAT;
  let A be bounded Subset of TOP-REAL n;
  cluster Fr A -> bounded;
end;

theorem :: JORDAN:25
  for A being closed Subset of TOP-REAL n, p being Point of TOP-REAL n st
  not p in A ex r being positive Real st Ball(p,r) misses A;

theorem :: JORDAN:26
  for A being bounded Subset of TOP-REAL n, a being Point of TOP-REAL n
  ex r being positive Real st A c= Ball(a,r);

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

registration
  let T be non empty T_2 TopSpace;
  cluster -> T_2 for non empty SubSpace of T;
end;

registration
  let p, r;
  cluster Tdisk(p,r) -> closed;
end;

registration
  let p, r;
  cluster Tdisk(p,r) -> compact;
end;

begin :: Paths

theorem :: JORDAN:28
  for T being non empty TopSpace, a, b being Point of T
  for f being Path of a,b st a,b are_connected holds rng f is connected;

theorem :: JORDAN:29
  for X being non empty TopSpace, Y being non empty SubSpace of X,
  x1, x2 being Point of X, y1, y2 being Point of Y,
  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;

theorem :: JORDAN:30
  for X being pathwise_connected non empty TopSpace,
  Y being non empty SubSpace of X,
  x1, x2 being Point of X, y1, y2 being Point of Y,
  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;

theorem :: JORDAN:31
  for T being non empty TopSpace, a, b being Point of T
  for f being Path of a,b st a,b are_connected holds rng f = rng -f;

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

theorem :: JORDAN:33
  for T being non empty TopSpace, a, b, c being Point of T
  for f being Path of a,b, g being Path of b,c st
  a,b are_connected & b,c are_connected holds rng f c= rng(f+g);

theorem :: JORDAN:34
  for T being pathwise_connected non empty TopSpace, a, b, c being Point of T
  for f being Path of a,b, g being Path of b,c holds rng f c= rng(f+g);

theorem :: JORDAN:35
  for T being non empty TopSpace, a, b, c being Point of T
  for f being Path of b,c, g being Path of a,b st
  a,b are_connected & b,c are_connected holds rng f c= rng(g+f);

theorem :: JORDAN:36
  for T being pathwise_connected non empty TopSpace, a, b, c being Point of T
  for f being Path of b,c, g being Path of a,b holds rng f c= rng(g+f);

theorem :: JORDAN:37
  for T being non empty TopSpace, a, b, c being Point of T
  for f being Path of a,b, g being Path of b,c st
  a,b are_connected & b,c are_connected holds rng(f+g) = rng f \/ rng g;

theorem :: JORDAN:38
  for T being pathwise_connected non empty TopSpace, a, b, c being Point of T
  for f being Path of a,b, g being Path of b,c holds rng(f+g) = rng f \/ rng g;

theorem :: JORDAN:39
  for T being non empty TopSpace, a, b, c, d being Point of T
  for f being Path of a,b, g being Path of b,c, 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;

theorem :: JORDAN:40
  for T being pathwise_connected non empty TopSpace,
      a, b, c, d being Point of T
  for f being Path of a,b, g being Path of b,c, h being Path of c,d
  holds rng(f+g+h) = rng f \/ rng g \/ rng h;

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

theorem :: JORDAN:42
  for p1, p2 being Point of TOP-REAL n, P being Subset of TOP-REAL n
  holds P is_an_arc_of p1,p2 implies
  ex F being Path of p1,p2, f being Function of I[01], (TOP-REAL n)|P st
  rng f = P & F = f;

theorem :: JORDAN:43
  for p1, p2 being Point of TOP-REAL n
  ex F being Path of p1,p2, f being Function
  of I[01], (TOP-REAL n)|LSeg(p1,p2) st rng f = LSeg(p1,p2) & F = f;

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

begin :: Rectangles

theorem :: JORDAN:45
  a <= b & c <= d implies
  rectangle(a,b,c,d) c= closed_inside_of_rectangle(a,b,c,d);

theorem :: JORDAN:46
  inside_of_rectangle(a,b,c,d) c= closed_inside_of_rectangle(a,b,c,d);

theorem :: JORDAN:47
  closed_inside_of_rectangle(a,b,c,d) = outside_of_rectangle(a,b,c,d)`;

registration
  let a, b, c, d be Real;
  cluster closed_inside_of_rectangle(a,b,c,d) -> closed;
end;

theorem :: JORDAN:48
  closed_inside_of_rectangle(a,b,c,d) misses outside_of_rectangle(a,b,c,d);

theorem :: JORDAN:49
  closed_inside_of_rectangle(a,b,c,d) /\ inside_of_rectangle(a,b,c,d)
  = inside_of_rectangle(a,b,c,d);

theorem :: JORDAN:50
  a < b & c < d implies
  Int closed_inside_of_rectangle(a,b,c,d) = inside_of_rectangle(a,b,c,d);

theorem :: JORDAN:51
  a <= b & c <= d implies
  closed_inside_of_rectangle(a,b,c,d) \ inside_of_rectangle(a,b,c,d)
  = rectangle(a,b,c,d);

theorem :: JORDAN:52
  a < b & c < d implies
  Fr closed_inside_of_rectangle(a,b,c,d) = rectangle(a,b,c,d);

theorem :: JORDAN:53
  a <= b & c <= d implies W-bound closed_inside_of_rectangle(a,b,c,d) = a;

theorem :: JORDAN:54
  a <= b & c <= d implies S-bound closed_inside_of_rectangle(a,b,c,d) = c;

theorem :: JORDAN:55
  a <= b & c <= d implies E-bound closed_inside_of_rectangle(a,b,c,d) = b;

theorem :: JORDAN:56
  a <= b & c <= d implies N-bound closed_inside_of_rectangle(a,b,c,d) = d;

theorem :: JORDAN:57
  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 implies
  Segment(P,p1,p2,p1,First_Point(P,p1,p2,rectangle(a,b,c,d))) c=
  closed_inside_of_rectangle(a,b,c,d);

begin :: Some useful functions

definition
  let S, T be non empty TopSpace, x be Point of [:S,T:];
  redefine func x`1 -> Element of S;
  redefine func x`2 -> Element of T;
end;

definition
  let o be Point of TOP-REAL 2;
  func diffX2_1(o) -> RealMap of [:TOP-REAL 2,TOP-REAL 2:] means
:: JORDAN:def 1

  for x being Point of [:TOP-REAL 2,TOP-REAL 2:] holds it.x = x`2`1 - o`1;
  func diffX2_2(o) -> RealMap of [:TOP-REAL 2,TOP-REAL 2:] means
:: JORDAN:def 2

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

definition
  func diffX1_X2_1 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means
:: JORDAN:def 3

  for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`1`1 - x`2`1;
  func diffX1_X2_2 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means
:: JORDAN:def 4

  for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`1`2 - x`2`2;
  func Proj2_1 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means
:: JORDAN:def 5

  for x being Point of [:TOP-REAL 2, TOP-REAL 2:] holds it.x = x`2`1;
  func Proj2_2 -> RealMap of [:TOP-REAL 2, TOP-REAL 2:] means
:: JORDAN:def 6

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

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

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

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

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

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

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

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

registration
  cluster diffX1_X2_1 -> continuous;
  cluster diffX1_X2_2 -> continuous;
  cluster Proj2_1 -> continuous;
  cluster Proj2_2 -> continuous;
end;

definition
  let n be non zero Element of NAT, o, p be Point of TOP-REAL n,
  r be positive Real such that
 p is Point of Tdisk(o,r);
  func DiskProj(o,r,p) -> Function
  of (TOP-REAL n)|(cl_Ball(o,r)\{p}), Tcircle(o,r) means
:: 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);
end;

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

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

definition
  let n be non zero Element of NAT, o, p be Point of TOP-REAL n,
  r be positive Real such that
 p in Ball(o,r);
  func RotateCircle(o,r,p) -> Function of Tcircle(o,r), Tcircle(o,r) means
:: 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);
end;

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

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

begin :: Jordan's Curve Theorem

theorem :: JORDAN:68
  U = P & U is a_component &
  V is a_component & U <> V implies Cl P misses V;

theorem :: JORDAN:69
  U is a_component implies
  (TOP-REAL 2)|C`|U is pathwise_connected;

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

theorem :: JORDAN:71
  |[-1,0]|,|[1,0]| realize-max-dist-in P implies
  P c= closed_inside_of_rectangle(-1,1,-3,3);

theorem :: JORDAN:72
  |[-1,0]|,|[1,0]| realize-max-dist-in P implies
  P misses LSeg(|[-1,3]|,|[1,3]|);

theorem :: JORDAN:73
  |[-1,0]|,|[1,0]| realize-max-dist-in P implies
  P misses LSeg(|[-1,-3]|,|[1,-3]|);

theorem :: JORDAN:74
  |[-1,0]|,|[1,0]| realize-max-dist-in P implies
  P /\ rectangle(-1,1,-3,3) = {|[-1,0]|,|[1,0]|};

theorem :: JORDAN:75
  |[-1,0]|,|[1,0]| realize-max-dist-in P implies W-bound P = -1;

theorem :: JORDAN:76
  |[-1,0]|,|[1,0]| realize-max-dist-in P implies E-bound P = 1;

theorem :: JORDAN:77
  for P being compact Subset of TOP-REAL 2 holds
  |[-1,0]|,|[1,0]| realize-max-dist-in P implies W-most P = {|[-1,0]|};

theorem :: JORDAN:78
  for P being compact Subset of TOP-REAL 2 holds
  |[-1,0]|,|[1,0]| realize-max-dist-in P implies E-most P = {|[1,0]|};

theorem :: JORDAN:79
  for P being compact Subset of TOP-REAL 2 holds
  |[-1,0]|,|[1,0]| realize-max-dist-in P implies
  W-min P = |[-1,0]| & W-max P = |[-1,0]|;

theorem :: JORDAN:80
  for P being compact Subset of TOP-REAL 2 holds
  |[-1,0]|,|[1,0]| realize-max-dist-in P implies
  E-min P = |[1,0]| & E-max P = |[1,0]|;

theorem :: JORDAN:81
  |[-1,0]|,|[1,0]| realize-max-dist-in P implies
  LSeg(|[0,3]|,UMP P) is vertical;

theorem :: JORDAN:82
  |[-1,0]|,|[1,0]| realize-max-dist-in P implies
  LSeg(LMP P,|[0,-3]|) is vertical;

theorem :: JORDAN:83
  |[-1,0]|,|[1,0]| realize-max-dist-in P & p in P implies p`2 < 3;

theorem :: JORDAN:84
  |[-1,0]|,|[1,0]| realize-max-dist-in P & p in P implies -3 < p`2;

theorem :: JORDAN:85
  |[-1,0]|,|[1,0]| realize-max-dist-in D & p in LSeg(|[0,3]|,UMP D) implies
  (UMP D)`2 <= p`2;

theorem :: JORDAN:86
  |[-1,0]|,|[1,0]| realize-max-dist-in D & p in LSeg(LMP D,|[0,-3]|) implies
  p`2 <= (LMP D)`2;

theorem :: JORDAN:87
  |[-1,0]|,|[1,0]| realize-max-dist-in D implies
  LSeg(|[0,3]|,UMP D) c= north_halfline UMP D;

theorem :: JORDAN:88
  |[-1,0]|,|[1,0]| realize-max-dist-in D implies
  LSeg(LMP D,|[0,-3]|) c= south_halfline LMP D;

theorem :: JORDAN:89
  |[-1,0]|,|[1,0]| realize-max-dist-in C & P is_inside_component_of C implies
  LSeg(|[0,3]|,UMP C) misses P;

theorem :: JORDAN:90
  |[-1,0]|,|[1,0]| realize-max-dist-in C & P is_inside_component_of C implies
  LSeg(LMP C,|[0,-3]|) misses P;

theorem :: JORDAN:91
  |[-1,0]|,|[1,0]| realize-max-dist-in D implies
  LSeg(|[0,3]|,UMP D) /\ D = {UMP D};

theorem :: JORDAN:92
  |[-1,0]|,|[1,0]| realize-max-dist-in D implies
  LSeg(|[0,-3]|,LMP D) /\ D = {LMP D};

theorem :: JORDAN:93
  P is compact &
  |[-1,0]|,|[1,0]| realize-max-dist-in P & A is_inside_component_of P implies
  A c= closed_inside_of_rectangle(-1,1,-3,3);

theorem :: JORDAN:94
  |[-1,0]|,|[1,0]| realize-max-dist-in C implies LSeg(|[0,3]|,|[0,-3]|) meets C
;

theorem :: JORDAN:95
  |[-1,0]|,|[1,0]| realize-max-dist-in C implies
  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
  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;

theorem :: JORDAN:96
  |[-1,0]|,|[1,0]| realize-max-dist-in C implies
  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`);

registration :: do not remove it
  let C;
  cluster BDD C -> non empty;
end;

theorem :: JORDAN:97
  U = P & U is a_component implies C = Fr P;

theorem :: JORDAN:98 :: Jordan's Curve Theorem
  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;

::$N Jordan Curve Theorem
theorem :: JORDAN:99
  for C being Simple_closed_curve holds C is Jordan;