:: The Ordering of Points on a Curve, Part {III}
::  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, TOPREAL2, PRE_TOPC, EUCLID, SUBSET_1, TOPREAL1, FUNCT_1,
      BORSUK_1, RELAT_1, REAL_1, TOPS_2, CARD_1, XXREAL_0, STRUCT_0, XXREAL_1,
      JORDAN3, PSCOMP_1, JORDAN6, ARYTM_3, XBOOLE_0, JORDAN17;
 notations ORDINAL1, SUBSET_1, NUMBERS, XREAL_0, REAL_1, RCOMP_1, STRUCT_0,
      RELAT_1, FUNCT_1, TOPREAL1, TOPREAL2, PRE_TOPC, TOPS_2, BORSUK_1, EUCLID,
      JORDAN5C, PSCOMP_1, JORDAN6, XXREAL_0;
 constructors REAL_1, RCOMP_1, TOPS_2, COMPTS_1, TOPMETR, TOPREAL1, PSCOMP_1,
      JORDAN5C, JORDAN6, COMPLEX1;
 registrations RELSET_1, XREAL_0, MEMBERED, TOPREAL2, EUCLID;
 requirements NUMERALS, REAL, SUBSET;


begin

reserve C, P for Simple_closed_curve,
  a, b, c, d, e for Point of TOP-REAL 2;

theorem :: JORDAN17:1
  for n being Element of NAT, a, p1, p2 being Point of TOP-REAL n,
  P being Subset of TOP-REAL n st a in P & P is_an_arc_of p1,p2 ex f being
Function of I[01], (TOP-REAL n)|P, r being Real st f is being_homeomorphism & f
  .0 = p1 & f.1 = p2 & 0 <= r & r <= 1 & f.r = a;

theorem :: JORDAN17:2
  LE W-min(P),E-max(P),P;

theorem :: JORDAN17:3
  LE a,E-max(P),P implies a in Upper_Arc(P);

theorem :: JORDAN17:4
  LE E-max(P),a,P implies a in Lower_Arc(P);

theorem :: JORDAN17:5
  LE a,W-min(P),P implies a in Lower_Arc(P);

theorem :: JORDAN17:6
  for P being Subset of TOP-REAL 2 st a <> b & P is_an_arc_of c,d &
  LE a,b,P,c,d holds ex e st a <> e & b <> e & LE a,e,P,c,d & LE e,b,P,c,d;

theorem :: JORDAN17:7
  a in P implies ex e st a <> e & LE a,e,P;

theorem :: JORDAN17:8
  a <> b & LE a,b,P implies ex c st c <> a & c <> b & LE a,c,P & LE c,b,P;

definition
  let P be Subset of TOP-REAL 2, a, b, c, d be Point of TOP-REAL 2;
  pred a,b,c,d are_in_this_order_on P means
:: JORDAN17:def 1

  LE a,b,P & LE b,c,P & LE c,
d,P or LE b,c,P & LE c,d,P & LE d,a,P or LE c,d,P & LE d,a,P & LE a,b,P or LE d
  ,a,P & LE a,b,P & LE b,c,P;
end;

theorem :: JORDAN17:9
  a in P implies a,a,a,a are_in_this_order_on P;

theorem :: JORDAN17:10
  a,b,c,d are_in_this_order_on P implies b,c,d,a are_in_this_order_on P;

theorem :: JORDAN17:11
  a,b,c,d are_in_this_order_on P implies c,d,a,b are_in_this_order_on P;

theorem :: JORDAN17:12
  a,b,c,d are_in_this_order_on P implies d,a,b,c are_in_this_order_on P;

theorem :: JORDAN17:13
  a <> b & a,b,c,d are_in_this_order_on P implies ex e st e <> a & e <>
  b & a,e,b,c are_in_this_order_on P;

theorem :: JORDAN17:14
  a <> b & a,b,c,d are_in_this_order_on P implies ex e st e <> a & e <>
  b & a,e,b,d are_in_this_order_on P;

theorem :: JORDAN17:15
  b <> c & a,b,c,d are_in_this_order_on P implies ex e st e <> b & e <>
  c & a,b,e,c are_in_this_order_on P;

theorem :: JORDAN17:16
  b <> c & a,b,c,d are_in_this_order_on P implies ex e st e <> b & e <>
  c & b,e,c,d are_in_this_order_on P;

theorem :: JORDAN17:17
  c <> d & a,b,c,d are_in_this_order_on P implies ex e st e <> c & e <>
  d & a,c,e,d are_in_this_order_on P;

theorem :: JORDAN17:18
  c <> d & a,b,c,d are_in_this_order_on P implies ex e st e <> c & e <>
  d & b,c,e,d are_in_this_order_on P;

theorem :: JORDAN17:19
  d <> a & a,b,c,d are_in_this_order_on P implies ex e st e <> d & e <>
  a & a,b,d,e are_in_this_order_on P;

theorem :: JORDAN17:20
  d <> a & a,b,c,d are_in_this_order_on P implies ex e st e <> d & e <>
  a & a,c,d,e are_in_this_order_on P;

theorem :: JORDAN17:21
  a <> c & a <> d & b <> d & a,b,c,d are_in_this_order_on P & b,a,c,d
  are_in_this_order_on P implies a = b;

theorem :: JORDAN17:22
  a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & c,b,a,d
  are_in_this_order_on P implies a = c;

theorem :: JORDAN17:23
  a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & d,b,c,a
  are_in_this_order_on P implies a = d;

theorem :: JORDAN17:24
  a <> c & a <> d & b <> d & a,b,c,d are_in_this_order_on P & a,c,b,d
  are_in_this_order_on P implies b = c;

theorem :: JORDAN17:25
  a <> b & b <> c & c <> d & a,b,c,d are_in_this_order_on P & a,d,c,b
  are_in_this_order_on P implies b = d;

theorem :: JORDAN17:26
  a <> b & a <> c & b <> d & a,b,c,d are_in_this_order_on P & a,b,d,c
  are_in_this_order_on P implies c = d;

theorem :: JORDAN17:27
  a in C & b in C & c in C & d in C implies a,b,c,d are_in_this_order_on
C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,
  b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b
  are_in_this_order_on C;