The abstract of the Mizar article:

The Ordering of Points on a Curve. Part III

by

Artur Kornilowicz

Received September 16, 2002

MML identifier: JORDAN17

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, PRE_TOPC, EUCLID, BORSUK_1, RCOMP_1, RELAT_1, BOOLE,
      SUBSET_1, FUNCT_1, TOPREAL1, TOPS_2, COMPTS_1, JORDAN3, PSCOMP_1,
      TOPREAL2, JORDAN6, JORDAN17;
 notation XBOOLE_0, ORDINAL1, XREAL_0, REAL_1, NAT_1, RCOMP_1, STRUCT_0,
      RELAT_1, FUNCT_1, TOPREAL1, TOPREAL2, PRE_TOPC, TOPS_2, COMPTS_1,
      BORSUK_1, EUCLID, JORDAN5C, PSCOMP_1, JORDAN6;
 constructors RCOMP_1, TOPREAL2, CONNSP_1, TOPS_2, REAL_1, TOPREAL1, JORDAN5C,
      TREAL_1, PSCOMP_1, JORDAN6, SPPOL_1;
 clusters EUCLID, PSCOMP_1, XREAL_0, RELSET_1, JORDAN1B, MEMBERED;
 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 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 map of I[01], (TOP-REAL n)|P,
     r being Real st
   f is_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 compact non empty 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;