:: The Ordering of Points on a Curve, Part {IV}
::  by Artur Korni{\l}owicz
::
:: Received September 16, 2002
:: Copyright (c) 2002-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, EUCLID, PRE_TOPC, TOPREAL2, RELAT_1, STRUCT_0,
      ARYTM_1, SQUARE_1, XBOOLE_0, FUNCT_1, TOPS_2, RCOMP_1, ORDINAL2,
      TOPREAL1, XXREAL_2, MCART_1, XXREAL_0, CARD_1, ARYTM_3, PCOMPS_1,
      METRIC_1, TARSKI, COMPLEX1, JORDAN2C, RLTOPSP1, SPPOL_1, ZFMISC_1,
      JORDAN6, JORDAN3, JORDAN18, SEQ_4, REAL_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, ORDINAL1,
      NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, XXREAL_2, SEQ_4,
      STRUCT_0, PCOMPS_1, COMPLEX1, PRE_TOPC, TOPS_2, RCOMP_1, COMPTS_1,
      METRIC_1, SPPOL_1, RLTOPSP1, EUCLID, TOPREAL1, PSCOMP_1, TOPREAL2,
      JORDAN5C, JORDAN2C, TOPREAL6, JORDAN6;
 constructors REAL_1, SQUARE_1, COMPLEX1, RCOMP_1, TOPS_2, COMPTS_1, TOPREAL1,
      SPPOL_1, PSCOMP_1, JORDAN5C, JORDAN6, JORDAN2C, TOPREAL6, SEQ_4,
      RELSET_1, FUNCSDOM, BINOP_2, PCOMPS_1;
 registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED,
      COMPTS_1, EUCLID, TOPREAL1, STRUCT_0, TOPS_1, JORDAN2C, ORDINAL1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin  :: Preliminaries

reserve n for Element of NAT,
  V for Subset of TOP-REAL n,
  s,s1,s2,t,t1,t2 for Point of TOP-REAL n,
  C for Simple_closed_curve,
  P for Subset of TOP-REAL 2,
  a,p ,p1,p2,q,q1,q2 for Point of TOP-REAL 2;

theorem :: JORDAN18:1
  for a,b being Real holds (a-b)^2 = (b-a)^2;

theorem :: JORDAN18:2
  for S,T being non empty TopStruct, f being Function of S,T, A being
  Subset of T st f is being_homeomorphism & A is compact holds f"A is compact;

theorem :: JORDAN18:3
  proj2.:(north_halfline a) is bounded_below;

theorem :: JORDAN18:4
  proj2.:(south_halfline a) is bounded_above;

theorem :: JORDAN18:5
  proj1.:(west_halfline a) is bounded_above;

theorem :: JORDAN18:6
  proj1.:(east_halfline a) is bounded_below;

registration
  let a;
  cluster proj2.:(north_halfline a) -> non empty;
  cluster proj2.:(south_halfline a) -> non empty;
  cluster proj1.:(west_halfline a) -> non empty;
  cluster proj1.:(east_halfline a) -> non empty;
end;

theorem :: JORDAN18:7
  lower_bound(proj2.:(north_halfline a)) = a`2;

theorem :: JORDAN18:8
  upper_bound(proj2.:(south_halfline a)) = a`2;

theorem :: JORDAN18:9
  upper_bound(proj1.:(west_halfline a)) = a`1;

theorem :: JORDAN18:10
  lower_bound(proj1.:(east_halfline a)) = a`1;

registration
  let a;
  cluster north_halfline a -> closed;
  cluster south_halfline a -> closed;
  cluster east_halfline a -> closed;
  cluster west_halfline a -> closed;
end;

theorem :: JORDAN18:11
  a in BDD P implies not north_halfline a c= UBD P;

theorem :: JORDAN18:12
  a in BDD P implies not south_halfline a c= UBD P;

theorem :: JORDAN18:13
  a in BDD P implies not east_halfline a c= UBD P;

theorem :: JORDAN18:14
  a in BDD P implies not west_halfline a c= UBD P;

theorem :: JORDAN18:15
  for C being Simple_closed_curve, P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & P c= C ex R being non
empty Subset of TOP-REAL 2 st R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,
  p2};

begin  :: Two Special Points on a Simple Closed Curve

definition
  let p,P;
  func North-Bound(p,P) -> Point of TOP-REAL 2 equals
:: JORDAN18:def 1
  |[p`1,lower_bound(proj2.:(P /\
  north_halfline p))]|;
  func South-Bound(p,P) -> Point of TOP-REAL 2 equals
:: JORDAN18:def 2
  |[p`1,upper_bound(proj2.:(P /\
  south_halfline p))]|;
end;

theorem :: JORDAN18:16
  North-Bound(p,P)`1 = p`1 & South-Bound(p,P)`1 = p`1;

theorem :: JORDAN18:17
  for C being compact Subset of TOP-REAL 2 holds p in BDD C
  implies North-Bound(p,C) in C & North-Bound(p,C) in north_halfline p &
  South-Bound(p,C) in C & South-Bound(p,C) in south_halfline p;

theorem :: JORDAN18:18
  for C being compact Subset of TOP-REAL 2 holds p in BDD C
  implies South-Bound(p,C)`2 < p`2 & p`2 < North-Bound(p,C)`2;

theorem :: JORDAN18:19
  for C being compact Subset of TOP-REAL 2 holds p in BDD C
implies lower_bound(proj2.:(C /\ north_halfline p)) >
 upper_bound(proj2.:(C /\ south_halfline p
  ));

theorem :: JORDAN18:20
  for C being compact Subset of TOP-REAL 2 holds p in BDD C implies
  South-Bound(p,C) <> North-Bound(p,C);

theorem :: JORDAN18:21
  for C being Subset of TOP-REAL 2 holds LSeg(North-Bound(p,C),
  South-Bound(p,C)) is vertical;

theorem :: JORDAN18:22
  for C being compact Subset of TOP-REAL 2 holds p in BDD C implies LSeg
(North-Bound(p,C),South-Bound(p,C)) /\ C = { North-Bound(p,C), South-Bound(p,C)
  };

theorem :: JORDAN18:23
  for C being compact Subset of TOP-REAL 2 holds p in BDD C & q in BDD C
  & p`1 <> q`1 implies North-Bound(p,C), South-Bound(q,C), North-Bound(q,C),
  South-Bound(p,C) are_mutually_distinct;

begin  :: An Order of Points on a Simple Closed Curve

definition
  let n,V,s1,s2,t1,t2;
  pred s1,s2, V-separate t1,t2 means
:: JORDAN18:def 3

  for A being Subset of TOP-REAL n
  st A is_an_arc_of s1,s2 & A c= V holds A meets {t1,t2};
end;

notation
  let n,V,s1,s2,t1,t2;
  antonym s1,s2 are_neighbours_wrt t1,t2, V for s1,s2, V-separate t1,t2;
end;

theorem :: JORDAN18:24
  t,t, V-separate s1,s2;

theorem :: JORDAN18:25
  s1,s2, V-separate t1,t2 implies s2,s1, V-separate t1,t2;

theorem :: JORDAN18:26
  s1,s2, V-separate t1,t2 implies s1,s2, V-separate t2,t1;

theorem :: JORDAN18:27
  s,t1, V-separate s,t2;

theorem :: JORDAN18:28
  t1,s, V-separate t2,s;

theorem :: JORDAN18:29
  t1,s, V-separate s,t2;

theorem :: JORDAN18:30
  s,t1, V-separate t2,s;

theorem :: JORDAN18:31
  for p1,p2,q being Point of TOP-REAL 2 st q in C & p1 in C & p2 in C &
  p1 <> p2 & p1 <> q & p2 <> q holds p1,p2 are_neighbours_wrt q,q, C;

theorem :: JORDAN18:32
  p1 <> p2 & p1 in C & p2 in C implies (p1,p2, C-separate q1,q2 implies
  q1,q2, C-separate p1,p2);

theorem :: JORDAN18:33
  p1 in C & p2 in C & q1 in C & p1 <> p2 & q1 <> p1 & q1 <> p2 & q2 <>
  p1 & q2 <> p2 implies p1,p2 are_neighbours_wrt q1,q2, C or p1,q1
  are_neighbours_wrt p2,q2, C;