:: 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

theorem Th1: :: JORDAN17:1

for n being Element of NAT
for a, p1, p2 being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st a in P & P is_an_arc_of p1,p2 holds
ex f being Function of I[01],((TOP-REAL n) | 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2)
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 being Point of (TOP-REAL 2) 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 (TOP-REAL 2) st a in P holds
ex e being Point of (TOP-REAL 2) 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 (TOP-REAL 2) st a <> b & LE a,b,P holds
ex c being Point of (TOP-REAL 2) st
( c <> a & c <> b & LE a,c,P & LE c,b,P )

proof end;

definition

let P be Subset of (TOP-REAL 2);
let 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;

:: deftheorem defines are_in_this_order_on JORDAN17:def 1 :
for P being Subset of (TOP-REAL 2)
for a, b, c, d being Point of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) st a <> b & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) 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 (TOP-REAL 2) st a <> b & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) 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 (TOP-REAL 2) st b <> c & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) 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 (TOP-REAL 2) st b <> c & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) 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 (TOP-REAL 2) st c <> d & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) 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 (TOP-REAL 2) st c <> d & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) 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 (TOP-REAL 2) st d <> a & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) 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 (TOP-REAL 2) st d <> a & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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 (TOP-REAL 2) 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;