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

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

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

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

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 )

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 )

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 )

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;

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

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;

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 ;

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 ;

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 ;

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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 )

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

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

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

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

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

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

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

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;