:: The Ordering of Points on a Curve, Part {III} :: by Artur Korni{\l}owicz :: :: Received September 16, 2002 :: Copyright (c) 2002-2012 Association of Mizar Users begin 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 ) proofend; theorem :: JORDAN17:2 for P being Simple_closed_curve holds LE W-min P, E-max P,P proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 ) proofend; definition let P be Subset of (TOP-REAL 2); let a, b, c, d be Point of (TOP-REAL 2); preda,b,c,d are_in_this_order_on P means :Def1: :: 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 Def1 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; theorem :: JORDAN17:15 for P being Simple_closed_curve for b, c, a, 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 ) proofend; theorem :: JORDAN17:16 for P being Simple_closed_curve for b, c, a, 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 ) proofend; theorem :: JORDAN17:17 for P being Simple_closed_curve for c, d, a, b 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 ) proofend; theorem :: JORDAN17:18 for P being Simple_closed_curve for c, d, a, b 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 ) proofend; theorem :: JORDAN17:19 for P being Simple_closed_curve for d, a, b, c 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 ) proofend; theorem :: JORDAN17:20 for P being Simple_closed_curve for d, a, b, c 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 ) proofend; theorem :: JORDAN17:21 for P being Simple_closed_curve for a, c, d, b 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 proofend; 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 proofend; 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 proofend; theorem :: JORDAN17:24 for P being Simple_closed_curve for a, c, d, b 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 proofend; 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 proofend; 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 proofend; 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 proofend;