Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

### The Ordering of Points on a Curve. Part III

by
Artur Kornilowicz

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