:: The Ordering of Points on a Curve, Part {III}
:: by Artur Korni{\l}owicz
::
:: Copyright (c) 2002-2021 Association of Mizar Users

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

theorem :: JORDAN17:2
for P being Simple_closed_curve holds LE W-min P, E-max P,P
proof end;

theorem :: JORDAN17:3
for P being Simple_closed_curve
for a being Point of () st LE a, E-max P,P holds
a in Upper_Arc P
proof end;

theorem :: JORDAN17:4
for P being Simple_closed_curve
for a being Point of () st LE E-max P,a,P holds
a in Lower_Arc P
proof end;

theorem :: JORDAN17:5
for P being Simple_closed_curve
for a being Point of () st LE a, W-min P,P holds
a in Lower_Arc P
proof end;

theorem Th6: :: JORDAN17:6
for a, b, c, d being Point of ()
for P being Subset of () st a <> b & P is_an_arc_of c,d & LE a,b,P,c,d holds
ex e being Point of () st
( a <> e & b <> e & LE a,e,P,c,d & LE e,b,P,c,d )
proof end;

theorem Th7: :: JORDAN17:7
for P being Simple_closed_curve
for a being Point of () st a in P holds
ex e being Point of () st
( a <> e & LE a,e,P )
proof end;

theorem Th8: :: JORDAN17:8
for P being Simple_closed_curve
for a, b being Point of () st a <> b & LE a,b,P holds
ex c being Point of () st
( c <> a & c <> b & LE a,c,P & LE c,b,P )
proof end;

definition
let P be Subset of ();
let a, b, c, d be Point of ();
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;

:: deftheorem defines are_in_this_order_on JORDAN17:def 1 :
for P being Subset of ()
for a, b, c, d being Point of () holds
( a,b,c,d are_in_this_order_on P iff ( ( 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 ) ) );

theorem :: JORDAN17:9
for P being Simple_closed_curve
for a being Point of () st a in P holds
a,a,a,a are_in_this_order_on P by JORDAN6:56;

theorem :: JORDAN17:10
for P being Simple_closed_curve
for a, b, c, d being Point of () st a,b,c,d are_in_this_order_on P holds
b,c,d,a are_in_this_order_on P ;

theorem :: JORDAN17:11
for P being Simple_closed_curve
for a, b, c, d being Point of () st a,b,c,d are_in_this_order_on P holds
c,d,a,b are_in_this_order_on P ;

theorem :: JORDAN17:12
for P being Simple_closed_curve
for a, b, c, d being Point of () st a,b,c,d are_in_this_order_on P holds
d,a,b,c are_in_this_order_on P ;

theorem :: JORDAN17:13
for P being Simple_closed_curve
for a, b, c, d being Point of () st a <> b & a,b,c,d are_in_this_order_on P holds
ex e being Point of () st
( e <> a & e <> b & a,e,b,c are_in_this_order_on P )
proof end;

theorem :: JORDAN17:14
for P being Simple_closed_curve
for a, b, c, d being Point of () st a <> b & a,b,c,d are_in_this_order_on P holds
ex e being Point of () st
( e <> a & e <> b & a,e,b,d are_in_this_order_on P )
proof end;

theorem :: JORDAN17:15
for P being Simple_closed_curve
for a, b, c, d being Point of () st b <> c & a,b,c,d are_in_this_order_on P holds
ex e being Point of () st
( e <> b & e <> c & a,b,e,c are_in_this_order_on P )
proof end;

theorem :: JORDAN17:16
for P being Simple_closed_curve
for a, b, c, d being Point of () st b <> c & a,b,c,d are_in_this_order_on P holds
ex e being Point of () st
( e <> b & e <> c & b,e,c,d are_in_this_order_on P )
proof end;

theorem :: JORDAN17:17
for P being Simple_closed_curve
for a, b, c, d being Point of () st c <> d & a,b,c,d are_in_this_order_on P holds
ex e being Point of () st
( e <> c & e <> d & a,c,e,d are_in_this_order_on P )
proof end;

theorem :: JORDAN17:18
for P being Simple_closed_curve
for a, b, c, d being Point of () st c <> d & a,b,c,d are_in_this_order_on P holds
ex e being Point of () st
( e <> c & e <> d & b,c,e,d are_in_this_order_on P )
proof end;

theorem :: JORDAN17:19
for P being Simple_closed_curve
for a, b, c, d being Point of () st d <> a & a,b,c,d are_in_this_order_on P holds
ex e being Point of () st
( e <> d & e <> a & a,b,d,e are_in_this_order_on P )
proof end;

theorem :: JORDAN17:20
for P being Simple_closed_curve
for a, b, c, d being Point of () st d <> a & a,b,c,d are_in_this_order_on P holds
ex e being Point of () st
( e <> d & e <> a & a,c,d,e are_in_this_order_on P )
proof end;

theorem :: JORDAN17:21
for P being Simple_closed_curve
for a, b, c, d being Point of () st 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 holds
a = b
proof end;

theorem :: JORDAN17:22
for P being Simple_closed_curve
for a, b, c, d being Point of () st 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 holds
a = c
proof end;

theorem :: JORDAN17:23
for P being Simple_closed_curve
for a, b, c, d being Point of () st 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 holds
a = d
proof end;

theorem :: JORDAN17:24
for P being Simple_closed_curve
for a, b, c, d being Point of () st 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 holds
b = c
proof end;

theorem :: JORDAN17:25
for P being Simple_closed_curve
for a, b, c, d being Point of () st 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 holds
b = d
proof end;

theorem :: JORDAN17:26
for P being Simple_closed_curve
for a, b, c, d being Point of () st 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 holds
c = d
proof end;

theorem :: JORDAN17:27
for C being Simple_closed_curve
for a, b, c, d being Point of () st a in C & b in C & c in C & d in C & not a,b,c,d are_in_this_order_on C & not a,b,d,c are_in_this_order_on C & not a,c,b,d are_in_this_order_on C & not a,c,d,b are_in_this_order_on C & not a,d,b,c are_in_this_order_on C holds
a,d,c,b are_in_this_order_on C
proof end;