jordan17.miz



    begin

    reserve C,P for Simple_closed_curve,

a,b,c,d,e for Point of ( TOP-REAL 2);

    theorem :: JORDAN17:1

    

     Th1: for n be Element of NAT , a,p1,p2 be Point of ( TOP-REAL n), P be Subset of ( TOP-REAL n) st a in P & P is_an_arc_of (p1,p2) holds ex f be Function of I[01] , (( TOP-REAL n) | P), r be Real st f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = p2 & 0 <= r & r <= 1 & (f . r) = a

    proof

      let n be Element of NAT , a,p1,p2 be Point of ( TOP-REAL n), P be Subset of ( TOP-REAL n) such that

       A1: a in P;

      given f be Function of I[01] , (( TOP-REAL n) | P) such that

       A2: f is being_homeomorphism and

       A3: (f . 0 ) = p1 & (f . 1) = p2;

      ( rng f) = ( [#] (( TOP-REAL n) | P)) by A2, TOPS_2:def 5

      .= the carrier of (( TOP-REAL n) | P)

      .= P by PRE_TOPC: 8;

      then

      consider r be object such that

       A4: r in ( dom f) and

       A5: a = (f . r) by A1, FUNCT_1:def 3;

      

       A6: ( dom f) = ( [#] I[01] ) by A2, TOPS_2:def 5

      .= [. 0 , 1.] by BORSUK_1: 40;

      then

      reconsider r as Real by A4;

      take f, r;

      thus f is being_homeomorphism & (f . 0 ) = p1 & (f . 1) = p2 by A2, A3;

      thus 0 <= r & r <= 1 by A4, A6, XXREAL_1: 1;

      thus thesis by A5;

    end;

    theorem :: JORDAN17:2

     LE (( W-min P),( E-max P),P)

    proof

      

       A1: ( E-max P) <> ( W-min P) by TOPREAL5: 19;

      ( W-min P) in ( Upper_Arc P) & ( E-max P) in ( Lower_Arc P) by JORDAN7: 1;

      hence thesis by A1, JORDAN6:def 10;

    end;

    theorem :: JORDAN17:3

     LE (a,( E-max P),P) implies a in ( Upper_Arc P)

    proof

      assume

       A1: LE (a,( E-max P),P);

      per cases by A1, JORDAN6:def 10;

        suppose a in ( Upper_Arc P) & ( E-max P) in ( Lower_Arc P) & not ( E-max P) = ( W-min P) or a in ( Upper_Arc P) & ( E-max P) in ( Upper_Arc P) & LE (a,( E-max P),( Upper_Arc P),( W-min P),( E-max P));

        hence thesis;

      end;

        suppose that

         A2: a in ( Lower_Arc P) and ( E-max P) in ( Lower_Arc P) & not ( E-max P) = ( W-min P) and

         A3: LE (a,( E-max P),( Lower_Arc P),( E-max P),( W-min P));

        ( Lower_Arc P) is_an_arc_of (( E-max P),( W-min P)) by JORDAN6:def 9;

        then

        consider f be Function of I[01] , (( TOP-REAL 2) | ( Lower_Arc P)), r be Real such that

         A4: f is being_homeomorphism and

         A5: (f . 0 ) = ( E-max P) and

         A6: (f . 1) = ( W-min P) and

         A7: 0 <= r and

         A8: r <= 1 and

         A9: (f . r) = a by A2, Th1;

        thus thesis

        proof

          per cases ;

            suppose r = 0 ;

            hence thesis by A5, A9, JORDAN7: 1;

          end;

            suppose r <> 0 ;

            then r > 0 by A7, XXREAL_0: 1;

            hence thesis by A3, A4, A5, A6, A8, A9, JORDAN5C:def 3;

          end;

        end;

      end;

    end;

    theorem :: JORDAN17:4

     LE (( E-max P),a,P) implies a in ( Lower_Arc P)

    proof

      assume

       A1: LE (( E-max P),a,P);

      per cases by A1, JORDAN6:def 10;

        suppose ( E-max P) in ( Upper_Arc P) & a in ( Lower_Arc P) & not a = ( W-min P) or ( E-max P) in ( Lower_Arc P) & a in ( Lower_Arc P) & not a = ( W-min P) & LE (( E-max P),a,( Lower_Arc P),( E-max P),( W-min P));

        hence thesis;

      end;

        suppose that ( E-max P) in ( Upper_Arc P) and

         A2: a in ( Upper_Arc P) and

         A3: LE (( E-max P),a,( Upper_Arc P),( W-min P),( E-max P));

        ( Upper_Arc P) is_an_arc_of (( W-min P),( E-max P)) by JORDAN6:def 8;

        then

        consider f be Function of I[01] , (( TOP-REAL 2) | ( Upper_Arc P)), r be Real such that

         A4: f is being_homeomorphism & (f . 0 ) = ( W-min P) and

         A5: (f . 1) = ( E-max P) and

         A6: 0 <= r and

         A7: r <= 1 and

         A8: (f . r) = a by A2, Th1;

        thus thesis

        proof

          per cases ;

            suppose r = 1;

            hence thesis by A5, A8, JORDAN7: 1;

          end;

            suppose r <> 1;

            then r < 1 by A7, XXREAL_0: 1;

            hence thesis by A3, A4, A5, A6, A8, JORDAN5C:def 3;

          end;

        end;

      end;

    end;

    theorem :: JORDAN17:5

     LE (a,( W-min P),P) implies a in ( Lower_Arc P)

    proof

      assume

       A1: LE (a,( W-min P),P);

      per cases by A1, JORDAN6:def 10;

        suppose a in ( Upper_Arc P) & ( W-min P) in ( Lower_Arc P) & not ( W-min P) = ( W-min P) or a in ( Lower_Arc P) & ( W-min P) in ( Lower_Arc P) & not ( W-min P) = ( W-min P) & LE (a,( W-min P),( Lower_Arc P),( E-max P),( W-min P));

        hence thesis;

      end;

        suppose that

         A2: a in ( Upper_Arc P) and ( W-min P) in ( Upper_Arc P) and

         A3: LE (a,( W-min P),( Upper_Arc P),( W-min P),( E-max P));

        ( Upper_Arc P) is_an_arc_of (( W-min P),( E-max P)) by JORDAN6:def 8;

        then

        consider f be Function of I[01] , (( TOP-REAL 2) | ( Upper_Arc P)), r be Real such that

         A4: f is being_homeomorphism and

         A5: (f . 0 ) = ( W-min P) and

         A6: (f . 1) = ( E-max P) and

         A7: 0 <= r and

         A8: r <= 1 and

         A9: (f . r) = a by A2, Th1;

        thus thesis

        proof

          per cases ;

            suppose r = 0 ;

            hence thesis by A5, A9, JORDAN7: 1;

          end;

            suppose r <> 0 ;

            then r > 0 by A7, XXREAL_0: 1;

            hence thesis by A3, A4, A5, A6, A8, A9, JORDAN5C:def 3;

          end;

        end;

      end;

    end;

    theorem :: JORDAN17:6

    

     Th6: for P be 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)

    proof

      let P be Subset of ( TOP-REAL 2);

      assume that

       A1: a <> b and

       A2: P is_an_arc_of (c,d) and

       A3: LE (a,b,P,c,d);

      b in P by A3, JORDAN5C:def 3;

      then

      consider f be Function of I[01] , (( TOP-REAL 2) | P), rb be Real such that

       A4: f is being_homeomorphism and

       A5: (f . 0 ) = c & (f . 1) = d and

       A6: 0 <= rb and

       A7: rb <= 1 and

       A8: (f . rb) = b by A2, Th1;

      

       A9: ( rng f) = ( [#] (( TOP-REAL 2) | P)) by A4, TOPS_2:def 5

      .= the carrier of (( TOP-REAL 2) | P)

      .= P by PRE_TOPC: 8;

      a in P by A3, JORDAN5C:def 3;

      then

      consider ra be object such that

       A10: ra in ( dom f) and

       A11: a = (f . ra) by A9, FUNCT_1:def 3;

      

       A12: ( dom f) = ( [#] I[01] ) by A4, TOPS_2:def 5

      .= [. 0 , 1.] by BORSUK_1: 40;

      then

      reconsider ra as Real by A10;

      

       A13: 0 <= ra by A10, A12, XXREAL_1: 1;

      

       A14: ra <= 1 by A10, A12, XXREAL_1: 1;

      then ra <= rb by A3, A4, A5, A6, A7, A8, A11, A13, JORDAN5C:def 3;

      then ra < rb by A1, A8, A11, XXREAL_0: 1;

      then

      consider re be Real such that

       A15: ra < re and

       A16: re < rb by XREAL_1: 5;

      set e = (f . re);

      

       A17: re <= 1 by A7, A16, XXREAL_0: 2;

      

       A18: 0 <= re by A13, A15, XXREAL_0: 2;

      then

       A19: re in ( dom f) by A12, A17, XXREAL_1: 1;

      then e in ( rng f) by FUNCT_1:def 3;

      then

      reconsider e as Point of ( TOP-REAL 2) by A9;

      take e;

      now

        assume

         A20: a = e or b = e;

        f is one-to-one & rb in ( dom f) by A4, A6, A7, A12, TOPS_2:def 5, XXREAL_1: 1;

        hence contradiction by A8, A10, A11, A15, A16, A19, A20, FUNCT_1:def 4;

      end;

      hence a <> e & b <> e;

      thus thesis by A2, A4, A5, A6, A7, A8, A11, A13, A14, A15, A16, A18, A17, JORDAN5C: 8;

    end;

    theorem :: JORDAN17:7

    

     Th7: a in P implies ex e st a <> e & LE (a,e,P)

    proof

      assume

       A1: a in P;

      

       A2: ( E-max P) <> ( W-min P) by TOPREAL5: 19;

      

       A3: ( Lower_Arc P) is_an_arc_of (( E-max P),( W-min P)) by JORDAN6:def 9;

      per cases ;

        suppose

         A4: a = ( W-min P);

        take ( E-max P);

        thus thesis by A4, JORDAN7: 3, SPRECT_1: 14, TOPREAL5: 19;

      end;

        suppose

         A5: a <> ( W-min P);

        thus thesis

        proof

          per cases ;

            suppose

             A6: a in ( Upper_Arc P);

            thus thesis

            proof

              per cases ;

                suppose

                 A7: a = ( E-max P);

                consider e such that

                 A8: e in ( Lower_Arc P) & e <> ( E-max P) & e <> ( W-min P) by A3, JORDAN6: 42;

                take e;

                thus thesis by A6, A7, A8, JORDAN6:def 10;

              end;

                suppose

                 A9: a <> ( E-max P);

                take ( E-max P);

                ( E-max P) in ( Lower_Arc P) by JORDAN7: 1;

                hence thesis by A2, A6, A9, JORDAN6:def 10;

              end;

            end;

          end;

            suppose

             A10: not a in ( Upper_Arc P);

            (( Upper_Arc P) \/ ( Lower_Arc P)) = P by JORDAN6:def 9;

            then

             A11: a in ( Lower_Arc P) by A1, A10, XBOOLE_0:def 3;

            then

            consider f be Function of I[01] , (( TOP-REAL 2) | ( Lower_Arc P)), r be Real such that

             A12: f is being_homeomorphism and

             A13: (f . 0 ) = ( E-max P) and

             A14: (f . 1) = ( W-min P) and

             A15: 0 <= r and

             A16: r <= 1 and

             A17: (f . r) = a by A3, Th1;

            

             A18: f is one-to-one by A12, TOPS_2:def 5;

            r < 1 by A5, A14, A16, A17, XXREAL_0: 1;

            then

            consider s be Real such that

             A19: r < s and

             A20: s < 1 by XREAL_1: 5;

            

             A21: ( dom f) = ( [#] I[01] ) by A12, TOPS_2:def 5

            .= [. 0 , 1.] by BORSUK_1: 40;

            

             A22: ( rng f) = ( [#] (( TOP-REAL 2) | ( Lower_Arc P))) by A12, TOPS_2:def 5

            .= the carrier of (( TOP-REAL 2) | ( Lower_Arc P))

            .= ( Lower_Arc P) by PRE_TOPC: 8;

            

             A23: 0 <= s by A15, A19, XXREAL_0: 2;

            then

             A24: s in ( dom f) by A21, A20, XXREAL_1: 1;

            then

             A25: (f . s) in ( rng f) by FUNCT_1:def 3;

            then

            reconsider e = (f . s) as Point of ( TOP-REAL 2) by A22;

            1 in ( dom f) by A21, XXREAL_1: 1;

            then

             A26: e <> ( W-min P) by A14, A18, A20, A24, FUNCT_1:def 4;

            take e;

            r in ( dom f) by A15, A16, A21, XXREAL_1: 1;

            hence a <> e by A17, A18, A19, A24, FUNCT_1:def 4;

             LE (a,e,( Lower_Arc P),( E-max P),( W-min P)) by A3, A12, A13, A14, A15, A16, A17, A19, A20, A23, JORDAN5C: 8;

            hence thesis by A11, A22, A25, A26, JORDAN6:def 10;

          end;

        end;

      end;

    end;

    theorem :: JORDAN17:8

    

     Th8: a <> b & LE (a,b,P) implies ex c st c <> a & c <> b & LE (a,c,P) & LE (c,b,P)

    proof

      assume that

       A1: a <> b and

       A2: LE (a,b,P);

      

       A3: ( Upper_Arc P) is_an_arc_of (( W-min P),( E-max P)) by JORDAN6:def 8;

      

       A4: ( Lower_Arc P) is_an_arc_of (( E-max P),( W-min P)) by JORDAN6:def 9;

      per cases by A2, JORDAN6:def 10;

        suppose that

         A5: a in ( Upper_Arc P) and

         A6: b in ( Lower_Arc P) and

         A7: not b = ( W-min P);

        

         A8: ( E-max P) in ( Lower_Arc P) by JORDAN7: 1;

        

         A9: ( E-max P) in ( Upper_Arc P) & ( E-max P) <> ( W-min P) by JORDAN7: 1, TOPREAL5: 19;

        thus thesis

        proof

          per cases ;

            suppose that

             A10: a <> ( E-max P) & b <> ( E-max P);

            take e = ( E-max P);

            thus a <> e & b <> e by A10;

            thus thesis by A5, A6, A7, A8, A9, JORDAN6:def 10;

          end;

            suppose

             A11: a = ( E-max P);

            then LE (a,b,( Lower_Arc P),( E-max P),( W-min P)) by A4, A6, JORDAN5C: 10;

            then

            consider e such that

             A12: a <> e & b <> e and

             A13: LE (a,e,( Lower_Arc P),( E-max P),( W-min P)) & LE (e,b,( Lower_Arc P),( E-max P),( W-min P)) by A1, A4, Th6;

            take e;

            thus e <> a & e <> b by A12;

            e in ( Lower_Arc P) & e <> ( W-min P) by A4, A7, A13, JORDAN5C:def 3, JORDAN6: 55;

            hence thesis by A6, A7, A8, A11, A13, JORDAN6:def 10;

          end;

            suppose

             A14: b = ( E-max P);

            then LE (a,b,( Upper_Arc P),( W-min P),( E-max P)) by A3, A5, JORDAN5C: 10;

            then

            consider e such that

             A15: a <> e & b <> e and

             A16: LE (a,e,( Upper_Arc P),( W-min P),( E-max P)) and LE (e,b,( Upper_Arc P),( W-min P),( E-max P)) by A1, A3, Th6;

            take e;

            thus e <> a & e <> b by A15;

            e in ( Upper_Arc P) by A16, JORDAN5C:def 3;

            hence thesis by A5, A7, A8, A14, A16, JORDAN6:def 10;

          end;

        end;

      end;

        suppose that

         A17: a in ( Upper_Arc P) & b in ( Upper_Arc P) and

         A18: LE (a,b,( Upper_Arc P),( W-min P),( E-max P));

        consider e such that

         A19: a <> e & b <> e and

         A20: LE (a,e,( Upper_Arc P),( W-min P),( E-max P)) and

         A21: LE (e,b,( Upper_Arc P),( W-min P),( E-max P)) by A1, A3, A18, Th6;

        take e;

        thus e <> a & e <> b by A19;

        e in ( Upper_Arc P) by A20, JORDAN5C:def 3;

        hence thesis by A17, A20, A21, JORDAN6:def 10;

      end;

        suppose that

         A22: a in ( Lower_Arc P) & b in ( Lower_Arc P) and

         A23: not b = ( W-min P) and

         A24: LE (a,b,( Lower_Arc P),( E-max P),( W-min P));

        consider e such that

         A25: a <> e & b <> e and

         A26: LE (a,e,( Lower_Arc P),( E-max P),( W-min P)) and

         A27: LE (e,b,( Lower_Arc P),( E-max P),( W-min P)) by A1, A4, A24, Th6;

        take e;

        thus e <> a & e <> b by A25;

        

         A28: e in ( Lower_Arc P) by A26, JORDAN5C:def 3;

        e <> ( W-min P) by A4, A23, A27, JORDAN6: 55;

        hence thesis by A22, A23, A26, A27, A28, JORDAN6:def 10;

      end;

    end;

    definition

      let P be Subset of ( TOP-REAL 2), a,b,c,d be Point of ( TOP-REAL 2);

      :: JORDAN17:def1

      pred a,b,c,d are_in_this_order_on P means 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 by JORDAN6: 56;

    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

    proof

      assume that

       A1: a <> b and

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

      per cases by A2;

        suppose

         A3: LE (a,b,P) & LE (b,c,P) & LE (c,d,P);

        then

        consider e such that

         A4: e <> a & e <> b & LE (a,e,P) & LE (e,b,P) by A1, Th8;

        take e;

        thus thesis by A3, A4;

      end;

        suppose that

         A5: LE (b,c,P) and

         A6: LE (c,d,P) and

         A7: LE (d,a,P);

        thus thesis

        proof

          

           A8: LE (c,a,P) by A6, A7, JORDAN6: 58;

          per cases ;

            suppose

             A9: b = ( W-min P);

            a in P by A7, JORDAN7: 5;

            then

            consider e such that

             A10: e <> a and

             A11: LE (a,e,P) by Th7;

            take e;

            thus e <> a by A10;

            thus e <> b by A1, A9, A11, JORDAN7: 2;

            thus thesis by A5, A8, A11;

          end;

            suppose

             A12: b <> ( W-min P);

            take e = ( W-min P);

            b in P by A5, JORDAN7: 5;

            then

             A13: LE (e,b,P) by JORDAN7: 3;

            now

               LE (b,d,P) by A5, A6, JORDAN6: 58;

              then

               A14: LE (b,a,P) by A7, JORDAN6: 58;

              assume e = a;

              hence contradiction by A1, A13, A14, JORDAN6: 57;

            end;

            hence e <> a;

            thus e <> b by A12;

            thus thesis by A5, A8, A13;

          end;

        end;

      end;

        suppose that

         A15: LE (c,d,P) and

         A16: LE (d,a,P) & LE (a,b,P);

        consider e such that

         A17: e <> a & e <> b & LE (a,e,P) & LE (e,b,P) by A1, A16, Th8;

        take e;

         LE (c,a,P) by A15, A16, JORDAN6: 58;

        hence thesis by A17;

      end;

        suppose that

         A18: LE (d,a,P) & LE (a,b,P) and

         A19: LE (b,c,P);

        consider e such that

         A20: e <> a & e <> b & LE (a,e,P) & LE (e,b,P) by A1, A18, Th8;

        take e;

        thus thesis by A19, A20;

      end;

    end;

    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

    proof

      assume that

       A1: a <> b and

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

      per cases by A2;

        suppose that

         A3: LE (a,b,P) and

         A4: LE (b,c,P) & LE (c,d,P);

        consider e such that

         A5: e <> a & e <> b & LE (a,e,P) & LE (e,b,P) by A1, A3, Th8;

        take e;

         LE (b,d,P) by A4, JORDAN6: 58;

        hence thesis by A5;

      end;

        suppose that

         A6: LE (b,c,P) and

         A7: LE (c,d,P) and

         A8: LE (d,a,P);

        thus thesis

        proof

          

           A9: LE (b,d,P) by A6, A7, JORDAN6: 58;

          per cases ;

            suppose

             A10: b = ( W-min P);

            a in P by A8, JORDAN7: 5;

            then

            consider e such that

             A11: e <> a and

             A12: LE (a,e,P) by Th7;

            take e;

            thus e <> a by A11;

            thus e <> b by A1, A10, A12, JORDAN7: 2;

            thus thesis by A8, A9, A12;

          end;

            suppose

             A13: b <> ( W-min P);

            take e = ( W-min P);

            b in P by A6, JORDAN7: 5;

            then

             A14: LE (e,b,P) by JORDAN7: 3;

            now

               LE (b,d,P) by A6, A7, JORDAN6: 58;

              then

               A15: LE (b,a,P) by A8, JORDAN6: 58;

              assume e = a;

              hence contradiction by A1, A14, A15, JORDAN6: 57;

            end;

            hence e <> a;

            thus e <> b by A13;

            thus thesis by A8, A9, A14;

          end;

        end;

      end;

        suppose that LE (c,d,P) and

         A16: LE (d,a,P) and

         A17: LE (a,b,P);

        consider e such that

         A18: e <> a & e <> b & LE (a,e,P) & LE (e,b,P) by A1, A17, Th8;

        take e;

        thus thesis by A16, A18;

      end;

        suppose that

         A19: LE (d,a,P) and

         A20: LE (a,b,P) and LE (b,c,P);

        consider e such that

         A21: e <> a & e <> b & LE (a,e,P) & LE (e,b,P) by A1, A20, Th8;

        take e;

        thus thesis by A19, A21;

      end;

    end;

    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

    proof

      assume that

       A1: b <> c and

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

      per cases by A2;

        suppose

         A3: LE (a,b,P) & LE (b,c,P) & LE (c,d,P);

        then

        consider e such that

         A4: e <> b & e <> c & LE (b,e,P) & LE (e,c,P) by A1, Th8;

        take e;

        thus thesis by A3, A4;

      end;

        suppose that

         A5: LE (b,c,P) and

         A6: LE (c,d,P) & LE (d,a,P);

        consider e such that

         A7: e <> b & e <> c & LE (b,e,P) & LE (e,c,P) by A1, A5, Th8;

        take e;

         LE (c,a,P) by A6, JORDAN6: 58;

        hence thesis by A7;

      end;

        suppose that

         A8: LE (c,d,P) and

         A9: LE (d,a,P) and

         A10: LE (a,b,P);

        thus thesis

        proof

          

           A11: LE (c,a,P) by A8, A9, JORDAN6: 58;

          per cases ;

            suppose

             A12: c = ( W-min P);

            b in P by A10, JORDAN7: 5;

            then

            consider e such that

             A13: e <> b and

             A14: LE (b,e,P) by Th7;

            take e;

            thus e <> b by A13;

            thus e <> c by A1, A12, A14, JORDAN7: 2;

            thus thesis by A10, A11, A14;

          end;

            suppose

             A15: c <> ( W-min P);

            take e = ( W-min P);

            c in P by A8, JORDAN7: 5;

            then

             A16: LE (e,c,P) by JORDAN7: 3;

            now

               LE (c,a,P) by A8, A9, JORDAN6: 58;

              then

               A17: LE (c,b,P) by A10, JORDAN6: 58;

              assume e = b;

              hence contradiction by A1, A16, A17, JORDAN6: 57;

            end;

            hence e <> b;

            thus e <> c by A15;

            thus thesis by A10, A11, A16;

          end;

        end;

      end;

        suppose that LE (d,a,P) and

         A18: LE (a,b,P) & LE (b,c,P);

        consider e such that

         A19: e <> b & e <> c & LE (b,e,P) & LE (e,c,P) by A1, A18, Th8;

        take e;

        thus thesis by A18, A19;

      end;

    end;

    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

    proof

      assume that

       A1: b <> c and

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

      per cases by A2;

        suppose

         A3: LE (a,b,P) & LE (b,c,P) & LE (c,d,P);

        then

        consider e such that

         A4: e <> b & e <> c & LE (b,e,P) & LE (e,c,P) by A1, Th8;

        take e;

        thus thesis by A3, A4;

      end;

        suppose

         A5: LE (b,c,P) & LE (c,d,P) & LE (d,a,P);

        then

        consider e such that

         A6: e <> b & e <> c & LE (b,e,P) & LE (e,c,P) by A1, Th8;

        take e;

        thus thesis by A5, A6;

      end;

        suppose that

         A7: LE (c,d,P) and

         A8: LE (d,a,P) and

         A9: LE (a,b,P);

        thus thesis

        proof

          

           A10: LE (d,b,P) by A8, A9, JORDAN6: 58;

          per cases ;

            suppose

             A11: c = ( W-min P);

            b in P by A9, JORDAN7: 5;

            then

            consider e such that

             A12: e <> b and

             A13: LE (b,e,P) by Th7;

            take e;

            thus e <> b by A12;

            thus e <> c by A1, A11, A13, JORDAN7: 2;

            thus thesis by A7, A10, A13;

          end;

            suppose

             A14: c <> ( W-min P);

            take e = ( W-min P);

            c in P by A7, JORDAN7: 5;

            then

             A15: LE (e,c,P) by JORDAN7: 3;

            now

               LE (c,a,P) by A7, A8, JORDAN6: 58;

              then

               A16: LE (c,b,P) by A9, JORDAN6: 58;

              assume e = b;

              hence contradiction by A1, A15, A16, JORDAN6: 57;

            end;

            hence e <> b;

            thus e <> c by A14;

            thus thesis by A7, A10, A15;

          end;

        end;

      end;

        suppose that

         A17: LE (d,a,P) & LE (a,b,P) and

         A18: LE (b,c,P);

        consider e such that

         A19: e <> b & e <> c and

         A20: LE (b,e,P) & LE (e,c,P) by A1, A18, Th8;

        take e;

        thus e <> b & e <> c by A19;

         LE (d,b,P) by A17, JORDAN6: 58;

        hence thesis by A20;

      end;

    end;

    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

    proof

      assume that

       A1: c <> d and

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

      per cases by A2;

        suppose that

         A3: LE (a,b,P) & LE (b,c,P) and

         A4: LE (c,d,P);

        consider e such that

         A5: e <> c & e <> d & LE (c,e,P) & LE (e,d,P) by A1, A4, Th8;

        take e;

         LE (a,c,P) by A3, JORDAN6: 58;

        hence thesis by A5;

      end;

        suppose that

         A6: LE (b,c,P) & LE (c,d,P) and

         A7: LE (d,a,P);

        consider e such that

         A8: e <> c & e <> d & LE (c,e,P) & LE (e,d,P) by A1, A6, Th8;

        take e;

        thus thesis by A7, A8;

      end;

        suppose that

         A9: LE (c,d,P) and

         A10: LE (d,a,P) and LE (a,b,P);

        consider e such that

         A11: e <> c & e <> d & LE (c,e,P) & LE (e,d,P) by A1, A9, Th8;

        take e;

        thus thesis by A10, A11;

      end;

        suppose that

         A12: LE (d,a,P) and

         A13: LE (a,b,P) and

         A14: LE (b,c,P);

        thus thesis

        proof

          

           A15: LE (a,c,P) by A13, A14, JORDAN6: 58;

          per cases ;

            suppose

             A16: d = ( W-min P);

            c in P by A14, JORDAN7: 5;

            then

            consider e such that

             A17: e <> c and

             A18: LE (c,e,P) by Th7;

            take e;

            thus e <> c by A17;

            thus e <> d by A1, A16, A18, JORDAN7: 2;

            thus thesis by A12, A15, A18;

          end;

            suppose

             A19: d <> ( W-min P);

            take e = ( W-min P);

            d in P by A12, JORDAN7: 5;

            then

             A20: LE (e,d,P) by JORDAN7: 3;

            now

               LE (d,b,P) by A12, A13, JORDAN6: 58;

              then

               A21: LE (d,c,P) by A14, JORDAN6: 58;

              assume e = c;

              hence contradiction by A1, A20, A21, JORDAN6: 57;

            end;

            hence e <> c;

            thus e <> d by A19;

            thus thesis by A12, A15, A20;

          end;

        end;

      end;

    end;

    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

    proof

      assume that

       A1: c <> d and

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

      per cases by A2;

        suppose that

         A3: LE (a,b,P) & LE (b,c,P) and

         A4: LE (c,d,P);

        consider e such that

         A5: e <> c & e <> d & LE (c,e,P) & LE (e,d,P) by A1, A4, Th8;

        take e;

        thus thesis by A3, A5;

      end;

        suppose that

         A6: LE (b,c,P) and

         A7: LE (c,d,P) and LE (d,a,P);

        consider e such that

         A8: e <> c & e <> d & LE (c,e,P) & LE (e,d,P) by A1, A7, Th8;

        take e;

        thus thesis by A6, A8;

      end;

        suppose that

         A9: LE (c,d,P) and

         A10: LE (d,a,P) & LE (a,b,P);

        consider e such that

         A11: e <> c & e <> d & LE (c,e,P) & LE (e,d,P) by A1, A9, Th8;

        take e;

         LE (d,b,P) by A10, JORDAN6: 58;

        hence thesis by A11;

      end;

        suppose that

         A12: LE (d,a,P) and

         A13: LE (a,b,P) and

         A14: LE (b,c,P);

        thus thesis

        proof

          

           A15: LE (d,b,P) by A12, A13, JORDAN6: 58;

          per cases ;

            suppose

             A16: d = ( W-min P);

            c in P by A14, JORDAN7: 5;

            then

            consider e such that

             A17: e <> c and

             A18: LE (c,e,P) by Th7;

            take e;

            thus e <> c by A17;

            thus e <> d by A1, A16, A18, JORDAN7: 2;

            thus thesis by A14, A15, A18;

          end;

            suppose

             A19: d <> ( W-min P);

            take e = ( W-min P);

            d in P by A12, JORDAN7: 5;

            then

             A20: LE (e,d,P) by JORDAN7: 3;

            now

              assume

               A21: e = c;

               LE (d,c,P) by A14, A15, JORDAN6: 58;

              hence contradiction by A1, A20, A21, JORDAN6: 57;

            end;

            hence e <> c;

            thus e <> d by A19;

            thus thesis by A14, A15, A20;

          end;

        end;

      end;

    end;

    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

    proof

      assume that

       A1: d <> a and

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

      per cases by A2;

        suppose that

         A3: LE (a,b,P) and

         A4: LE (b,c,P) and

         A5: LE (c,d,P);

        thus thesis

        proof

          

           A6: LE (b,d,P) by A4, A5, JORDAN6: 58;

          per cases ;

            suppose

             A7: a = ( W-min P);

            d in P by A5, JORDAN7: 5;

            then

            consider e such that

             A8: e <> d and

             A9: LE (d,e,P) by Th7;

            take e;

            thus e <> d by A8;

            thus e <> a by A1, A7, A9, JORDAN7: 2;

            thus thesis by A3, A6, A9;

          end;

            suppose

             A10: a <> ( W-min P);

            take e = ( W-min P);

            a in P by A3, JORDAN7: 5;

            then

             A11: LE (e,a,P) by JORDAN7: 3;

            now

               LE (a,c,P) by A3, A4, JORDAN6: 58;

              then

               A12: LE (a,d,P) by A5, JORDAN6: 58;

              assume e = d;

              hence contradiction by A1, A11, A12, JORDAN6: 57;

            end;

            hence e <> d;

            thus e <> a by A10;

            thus thesis by A3, A6, A11;

          end;

        end;

      end;

        suppose that

         A13: LE (b,c,P) & LE (c,d,P) and

         A14: LE (d,a,P);

        consider e such that

         A15: e <> d & e <> a & LE (d,e,P) & LE (e,a,P) by A1, A14, Th8;

        take e;

         LE (b,d,P) by A13, JORDAN6: 58;

        hence thesis by A15;

      end;

        suppose that LE (c,d,P) and

         A16: LE (d,a,P) and

         A17: LE (a,b,P);

        consider e such that

         A18: e <> d & e <> a & LE (d,e,P) & LE (e,a,P) by A1, A16, Th8;

        take e;

        thus thesis by A17, A18;

      end;

        suppose that

         A19: LE (d,a,P) and

         A20: LE (a,b,P) and LE (b,c,P);

        consider e such that

         A21: e <> d & e <> a & LE (d,e,P) & LE (e,a,P) by A1, A19, Th8;

        take e;

        thus thesis by A20, A21;

      end;

    end;

    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

    proof

      assume that

       A1: d <> a and

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

      per cases by A2;

        suppose that

         A3: LE (a,b,P) and

         A4: LE (b,c,P) and

         A5: LE (c,d,P);

        thus thesis

        proof

          

           A6: LE (a,c,P) by A3, A4, JORDAN6: 58;

          per cases ;

            suppose

             A7: a = ( W-min P);

            d in P by A5, JORDAN7: 5;

            then

            consider e such that

             A8: e <> d and

             A9: LE (d,e,P) by Th7;

            take e;

            thus e <> d by A8;

            thus e <> a by A1, A7, A9, JORDAN7: 2;

            thus thesis by A5, A6, A9;

          end;

            suppose

             A10: a <> ( W-min P);

            take e = ( W-min P);

            a in P by A3, JORDAN7: 5;

            then

             A11: LE (e,a,P) by JORDAN7: 3;

            now

              assume

               A12: e = d;

               LE (a,d,P) by A5, A6, JORDAN6: 58;

              hence contradiction by A1, A11, A12, JORDAN6: 57;

            end;

            hence e <> d;

            thus e <> a by A10;

            thus thesis by A5, A6, A11;

          end;

        end;

      end;

        suppose that LE (b,c,P) and

         A13: LE (c,d,P) and

         A14: LE (d,a,P);

        consider e such that

         A15: e <> d & e <> a & LE (d,e,P) & LE (e,a,P) by A1, A14, Th8;

        take e;

        thus thesis by A13, A15;

      end;

        suppose that

         A16: LE (c,d,P) and

         A17: LE (d,a,P) and LE (a,b,P);

        consider e such that

         A18: e <> d & e <> a & LE (d,e,P) & LE (e,a,P) by A1, A17, Th8;

        take e;

        thus thesis by A16, A18;

      end;

        suppose that

         A19: LE (d,a,P) and

         A20: LE (a,b,P) & LE (b,c,P);

        consider e such that

         A21: e <> d & e <> a & LE (d,e,P) & LE (e,a,P) by A1, A19, Th8;

        take e;

         LE (a,c,P) by A20, JORDAN6: 58;

        hence thesis by A21;

      end;

    end;

    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

    proof

      assume that

       A1: a <> c and

       A2: a <> d and

       A3: b <> d and

       A4: (a,b,c,d) are_in_this_order_on P and

       A5: (b,a,c,d) are_in_this_order_on P;

      per cases by A4;

        suppose

         A6: LE (a,b,P) & LE (b,c,P) & LE (c,d,P);

        then

         A7: LE (b,d,P) by JORDAN6: 58;

        thus thesis

        proof

          per cases by A5;

            suppose LE (b,a,P) & LE (a,c,P) & LE (c,d,P);

            hence thesis by A6, JORDAN6: 57;

          end;

            suppose LE (a,c,P) & LE (c,d,P) & LE (d,b,P);

            hence thesis by A3, A7, JORDAN6: 57;

          end;

            suppose LE (c,d,P) & LE (d,b,P) & LE (b,a,P);

            hence thesis by A6, JORDAN6: 57;

          end;

            suppose LE (d,b,P) & LE (b,a,P) & LE (a,c,P);

            hence thesis by A6, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A8: LE (b,c,P) & LE (c,d,P) & LE (d,a,P);

        then

         A9: LE (b,d,P) by JORDAN6: 58;

        thus thesis

        proof

          per cases by A5;

            suppose

             A10: LE (b,a,P) & LE (a,c,P) & LE (c,d,P);

             LE (c,a,P) by A8, JORDAN6: 58;

            hence thesis by A1, A10, JORDAN6: 57;

          end;

            suppose LE (a,c,P) & LE (c,d,P) & LE (d,b,P);

            hence thesis by A3, A9, JORDAN6: 57;

          end;

            suppose LE (c,d,P) & LE (d,b,P) & LE (b,a,P);

            hence thesis by A3, A9, JORDAN6: 57;

          end;

            suppose LE (d,b,P) & LE (b,a,P) & LE (a,c,P);

            hence thesis by A3, A9, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A11: LE (c,d,P) & LE (d,a,P) & LE (a,b,P);

        then

         A12: LE (c,a,P) by JORDAN6: 58;

        thus thesis

        proof

          per cases by A5;

            suppose LE (b,a,P) & LE (a,c,P) & LE (c,d,P);

            hence thesis by A11, JORDAN6: 57;

          end;

            suppose LE (a,c,P) & LE (c,d,P) & LE (d,b,P);

            hence thesis by A1, A12, JORDAN6: 57;

          end;

            suppose LE (c,d,P) & LE (d,b,P) & LE (b,a,P);

            hence thesis by A11, JORDAN6: 57;

          end;

            suppose LE (d,b,P) & LE (b,a,P) & LE (a,c,P);

            hence thesis by A11, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A13: LE (d,a,P) & LE (a,b,P) & LE (b,c,P);

        thus thesis

        proof

          per cases by A5;

            suppose LE (b,a,P) & LE (a,c,P) & LE (c,d,P);

            hence thesis by A13, JORDAN6: 57;

          end;

            suppose LE (a,c,P) & LE (c,d,P) & LE (d,b,P);

            then LE (a,d,P) by JORDAN6: 58;

            hence thesis by A2, A13, JORDAN6: 57;

          end;

            suppose LE (c,d,P) & LE (d,b,P) & LE (b,a,P);

            hence thesis by A13, JORDAN6: 57;

          end;

            suppose LE (d,b,P) & LE (b,a,P) & LE (a,c,P);

            hence thesis by A13, JORDAN6: 57;

          end;

        end;

      end;

    end;

    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

    proof

      assume that

       A1: a <> b and

       A2: b <> c and

       A3: c <> d and

       A4: (a,b,c,d) are_in_this_order_on P and

       A5: (c,b,a,d) are_in_this_order_on P;

      per cases by A4;

        suppose

         A6: LE (a,b,P) & LE (b,c,P) & LE (c,d,P);

        thus thesis

        proof

          per cases by A5;

            suppose LE (c,b,P) & LE (b,a,P) & LE (a,d,P);

            hence thesis by A1, A6, JORDAN6: 57;

          end;

            suppose LE (b,a,P) & LE (a,d,P) & LE (d,c,P);

            hence thesis by A3, A6, JORDAN6: 57;

          end;

            suppose LE (a,d,P) & LE (d,c,P) & LE (c,b,P);

            hence thesis by A3, A6, JORDAN6: 57;

          end;

            suppose LE (d,c,P) & LE (c,b,P) & LE (b,a,P);

            hence thesis by A3, A6, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A7: LE (b,c,P) & LE (c,d,P) & LE (d,a,P);

        thus thesis

        proof

          per cases by A5;

            suppose LE (c,b,P) & LE (b,a,P) & LE (a,d,P);

            hence thesis by A2, A7, JORDAN6: 57;

          end;

            suppose LE (b,a,P) & LE (a,d,P) & LE (d,c,P);

            hence thesis by A3, A7, JORDAN6: 57;

          end;

            suppose LE (a,d,P) & LE (d,c,P) & LE (c,b,P);

            hence thesis by A3, A7, JORDAN6: 57;

          end;

            suppose LE (d,c,P) & LE (c,b,P) & LE (b,a,P);

            hence thesis by A3, A7, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A8: LE (c,d,P) & LE (d,a,P) & LE (a,b,P);

        thus thesis

        proof

          per cases by A5;

            suppose LE (c,b,P) & LE (b,a,P) & LE (a,d,P);

            hence thesis by A1, A8, JORDAN6: 57;

          end;

            suppose LE (b,a,P) & LE (a,d,P) & LE (d,c,P);

            hence thesis by A3, A8, JORDAN6: 57;

          end;

            suppose LE (a,d,P) & LE (d,c,P) & LE (c,b,P);

            hence thesis by A3, A8, JORDAN6: 57;

          end;

            suppose LE (d,c,P) & LE (c,b,P) & LE (b,a,P);

            hence thesis by A3, A8, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A9: LE (d,a,P) & LE (a,b,P) & LE (b,c,P);

        thus thesis

        proof

          per cases by A5;

            suppose LE (c,b,P) & LE (b,a,P) & LE (a,d,P);

            hence thesis by A2, A9, JORDAN6: 57;

          end;

            suppose LE (b,a,P) & LE (a,d,P) & LE (d,c,P);

            hence thesis by A1, A9, JORDAN6: 57;

          end;

            suppose LE (a,d,P) & LE (d,c,P) & LE (c,b,P);

            hence thesis by A2, A9, JORDAN6: 57;

          end;

            suppose LE (d,c,P) & LE (c,b,P) & LE (b,a,P);

            hence thesis by A1, A9, JORDAN6: 57;

          end;

        end;

      end;

    end;

    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

    proof

      assume that

       A1: a <> b and

       A2: a <> c and

       A3: b <> d and

       A4: (a,b,c,d) are_in_this_order_on P and

       A5: (d,b,c,a) are_in_this_order_on P;

      per cases by A4;

        suppose

         A6: LE (a,b,P) & LE (b,c,P) & LE (c,d,P);

        then

         A7: LE (a,c,P) by JORDAN6: 58;

        thus thesis

        proof

          per cases by A5;

            suppose LE (d,b,P) & LE (b,c,P) & LE (c,a,P);

            hence thesis by A2, A7, JORDAN6: 57;

          end;

            suppose LE (b,c,P) & LE (c,a,P) & LE (a,d,P);

            hence thesis by A2, A7, JORDAN6: 57;

          end;

            suppose LE (c,a,P) & LE (a,d,P) & LE (d,b,P);

            hence thesis by A2, A7, JORDAN6: 57;

          end;

            suppose

             A8: LE (a,d,P) & LE (d,b,P) & LE (b,c,P);

             LE (b,d,P) by A6, JORDAN6: 58;

            hence thesis by A3, A8, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A9: LE (b,c,P) & LE (c,d,P) & LE (d,a,P);

        then

         A10: LE (b,d,P) by JORDAN6: 58;

        thus thesis

        proof

          per cases by A5;

            suppose LE (d,b,P) & LE (b,c,P) & LE (c,a,P);

            hence thesis by A3, A10, JORDAN6: 57;

          end;

            suppose LE (b,c,P) & LE (c,a,P) & LE (a,d,P);

            hence thesis by A9, JORDAN6: 57;

          end;

            suppose LE (c,a,P) & LE (a,d,P) & LE (d,b,P);

            hence thesis by A9, JORDAN6: 57;

          end;

            suppose LE (a,d,P) & LE (d,b,P) & LE (b,c,P);

            hence thesis by A9, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A11: LE (c,d,P) & LE (d,a,P) & LE (a,b,P);

        thus thesis

        proof

          per cases by A5;

            suppose LE (d,b,P) & LE (b,c,P) & LE (c,a,P);

            then LE (b,a,P) by JORDAN6: 58;

            hence thesis by A1, A11, JORDAN6: 57;

          end;

            suppose LE (b,c,P) & LE (c,a,P) & LE (a,d,P);

            hence thesis by A11, JORDAN6: 57;

          end;

            suppose LE (c,a,P) & LE (a,d,P) & LE (d,b,P);

            hence thesis by A11, JORDAN6: 57;

          end;

            suppose LE (a,d,P) & LE (d,b,P) & LE (b,c,P);

            hence thesis by A11, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A12: LE (d,a,P) & LE (a,b,P) & LE (b,c,P);

        thus thesis

        proof

          per cases by A5;

            suppose

             A13: LE (d,b,P) & LE (b,c,P) & LE (c,a,P);

             LE (a,c,P) by A12, JORDAN6: 58;

            hence thesis by A2, A13, JORDAN6: 57;

          end;

            suppose LE (b,c,P) & LE (c,a,P) & LE (a,d,P);

            hence thesis by A12, JORDAN6: 57;

          end;

            suppose LE (c,a,P) & LE (a,d,P) & LE (d,b,P);

            hence thesis by A12, JORDAN6: 57;

          end;

            suppose LE (a,d,P) & LE (d,b,P) & LE (b,c,P);

            hence thesis by A12, JORDAN6: 57;

          end;

        end;

      end;

    end;

    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

    proof

      assume that

       A1: a <> c and

       A2: a <> d and

       A3: b <> d and

       A4: (a,b,c,d) are_in_this_order_on P and

       A5: (a,c,b,d) are_in_this_order_on P;

      per cases by A4;

        suppose

         A6: LE (a,b,P) & LE (b,c,P) & LE (c,d,P);

        then

         A7: LE (b,d,P) by JORDAN6: 58;

        thus thesis

        proof

          per cases by A5;

            suppose LE (a,c,P) & LE (c,b,P) & LE (b,d,P);

            hence thesis by A6, JORDAN6: 57;

          end;

            suppose LE (c,b,P) & LE (b,d,P) & LE (d,a,P);

            hence thesis by A6, JORDAN6: 57;

          end;

            suppose

             A8: LE (b,d,P) & LE (d,a,P) & LE (a,c,P);

             LE (a,d,P) by A6, A7, JORDAN6: 58;

            hence thesis by A2, A8, JORDAN6: 57;

          end;

            suppose LE (d,a,P) & LE (a,c,P) & LE (c,b,P);

            hence thesis by A6, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A9: LE (b,c,P) & LE (c,d,P) & LE (d,a,P);

        then

         A10: LE (c,a,P) by JORDAN6: 58;

        thus thesis

        proof

          per cases by A5;

            suppose LE (a,c,P) & LE (c,b,P) & LE (b,d,P);

            hence thesis by A9, JORDAN6: 57;

          end;

            suppose LE (c,b,P) & LE (b,d,P) & LE (d,a,P);

            hence thesis by A9, JORDAN6: 57;

          end;

            suppose LE (b,d,P) & LE (d,a,P) & LE (a,c,P);

            hence thesis by A1, A10, JORDAN6: 57;

          end;

            suppose LE (d,a,P) & LE (a,c,P) & LE (c,b,P);

            hence thesis by A9, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A11: LE (c,d,P) & LE (d,a,P) & LE (a,b,P);

        then

         A12: LE (c,a,P) by JORDAN6: 58;

        thus thesis

        proof

          per cases by A5;

            suppose LE (a,c,P) & LE (c,b,P) & LE (b,d,P);

            hence thesis by A1, A12, JORDAN6: 57;

          end;

            suppose

             A13: LE (c,b,P) & LE (b,d,P) & LE (d,a,P);

             LE (d,b,P) by A11, JORDAN6: 58;

            hence thesis by A3, A13, JORDAN6: 57;

          end;

            suppose LE (b,d,P) & LE (d,a,P) & LE (a,c,P);

            hence thesis by A1, A12, JORDAN6: 57;

          end;

            suppose LE (d,a,P) & LE (a,c,P) & LE (c,b,P);

            hence thesis by A1, A12, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A14: LE (d,a,P) & LE (a,b,P) & LE (b,c,P);

        thus thesis

        proof

          per cases by A5;

            suppose LE (a,c,P) & LE (c,b,P) & LE (b,d,P);

            hence thesis by A14, JORDAN6: 57;

          end;

            suppose LE (c,b,P) & LE (b,d,P) & LE (d,a,P);

            hence thesis by A14, JORDAN6: 57;

          end;

            suppose

             A15: LE (b,d,P) & LE (d,a,P) & LE (a,c,P);

             LE (d,b,P) by A14, JORDAN6: 58;

            hence thesis by A3, A15, JORDAN6: 57;

          end;

            suppose LE (d,a,P) & LE (a,c,P) & LE (c,b,P);

            hence thesis by A14, JORDAN6: 57;

          end;

        end;

      end;

    end;

    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

    proof

      assume that

       A1: a <> b and

       A2: b <> c and

       A3: c <> d and

       A4: (a,b,c,d) are_in_this_order_on P and

       A5: (a,d,c,b) are_in_this_order_on P;

      per cases by A4;

        suppose

         A6: LE (a,b,P) & LE (b,c,P) & LE (c,d,P);

        thus thesis

        proof

          per cases by A5;

            suppose LE (a,d,P) & LE (d,c,P) & LE (c,b,P);

            hence thesis by A2, A6, JORDAN6: 57;

          end;

            suppose LE (d,c,P) & LE (c,b,P) & LE (b,a,P);

            hence thesis by A3, A6, JORDAN6: 57;

          end;

            suppose LE (c,b,P) & LE (b,a,P) & LE (a,d,P);

            hence thesis by A2, A6, JORDAN6: 57;

          end;

            suppose LE (b,a,P) & LE (a,d,P) & LE (d,c,P);

            hence thesis by A3, A6, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A7: LE (b,c,P) & LE (c,d,P) & LE (d,a,P);

        thus thesis

        proof

          per cases by A5;

            suppose LE (a,d,P) & LE (d,c,P) & LE (c,b,P);

            hence thesis by A3, A7, JORDAN6: 57;

          end;

            suppose LE (d,c,P) & LE (c,b,P) & LE (b,a,P);

            hence thesis by A3, A7, JORDAN6: 57;

          end;

            suppose LE (c,b,P) & LE (b,a,P) & LE (a,d,P);

            hence thesis by A2, A7, JORDAN6: 57;

          end;

            suppose LE (b,a,P) & LE (a,d,P) & LE (d,c,P);

            hence thesis by A3, A7, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A8: LE (c,d,P) & LE (d,a,P) & LE (a,b,P);

        thus thesis

        proof

          per cases by A5;

            suppose LE (a,d,P) & LE (d,c,P) & LE (c,b,P);

            hence thesis by A3, A8, JORDAN6: 57;

          end;

            suppose LE (d,c,P) & LE (c,b,P) & LE (b,a,P);

            hence thesis by A1, A8, JORDAN6: 57;

          end;

            suppose LE (c,b,P) & LE (b,a,P) & LE (a,d,P);

            hence thesis by A1, A8, JORDAN6: 57;

          end;

            suppose LE (b,a,P) & LE (a,d,P) & LE (d,c,P);

            hence thesis by A1, A8, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A9: LE (d,a,P) & LE (a,b,P) & LE (b,c,P);

        thus thesis

        proof

          per cases by A5;

            suppose LE (a,d,P) & LE (d,c,P) & LE (c,b,P);

            hence thesis by A2, A9, JORDAN6: 57;

          end;

            suppose LE (d,c,P) & LE (c,b,P) & LE (b,a,P);

            hence thesis by A2, A9, JORDAN6: 57;

          end;

            suppose LE (c,b,P) & LE (b,a,P) & LE (a,d,P);

            hence thesis by A2, A9, JORDAN6: 57;

          end;

            suppose LE (b,a,P) & LE (a,d,P) & LE (d,c,P);

            hence thesis by A1, A9, JORDAN6: 57;

          end;

        end;

      end;

    end;

    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

    proof

      assume that

       A1: a <> b and

       A2: a <> c and

       A3: b <> d and

       A4: (a,b,c,d) are_in_this_order_on P and

       A5: (a,b,d,c) are_in_this_order_on P;

      per cases by A4;

        suppose

         A6: LE (a,b,P) & LE (b,c,P) & LE (c,d,P);

        thus thesis

        proof

          per cases by A5;

            suppose LE (a,b,P) & LE (b,d,P) & LE (d,c,P);

            hence thesis by A6, JORDAN6: 57;

          end;

            suppose LE (b,d,P) & LE (d,c,P) & LE (c,a,P);

            hence thesis by A6, JORDAN6: 57;

          end;

            suppose LE (d,c,P) & LE (c,a,P) & LE (a,b,P);

            hence thesis by A6, JORDAN6: 57;

          end;

            suppose

             A7: LE (c,a,P) & LE (a,b,P) & LE (b,d,P);

             LE (a,c,P) by A6, JORDAN6: 58;

            hence thesis by A2, A7, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A8: LE (b,c,P) & LE (c,d,P) & LE (d,a,P);

        then

         A9: LE (c,a,P) by JORDAN6: 58;

        thus thesis

        proof

          per cases by A5;

            suppose LE (a,b,P) & LE (b,d,P) & LE (d,c,P);

            hence thesis by A8, JORDAN6: 57;

          end;

            suppose LE (b,d,P) & LE (d,c,P) & LE (c,a,P);

            hence thesis by A8, JORDAN6: 57;

          end;

            suppose LE (d,c,P) & LE (c,a,P) & LE (a,b,P);

            hence thesis by A8, JORDAN6: 57;

          end;

            suppose

             A10: LE (c,a,P) & LE (a,b,P) & LE (b,d,P);

             LE (b,a,P) by A8, A9, JORDAN6: 58;

            hence thesis by A1, A10, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A11: LE (c,d,P) & LE (d,a,P) & LE (a,b,P);

        then

         A12: LE (d,b,P) by JORDAN6: 58;

        thus thesis

        proof

          per cases by A5;

            suppose LE (a,b,P) & LE (b,d,P) & LE (d,c,P);

            hence thesis by A11, JORDAN6: 57;

          end;

            suppose LE (b,d,P) & LE (d,c,P) & LE (c,a,P);

            hence thesis by A11, JORDAN6: 57;

          end;

            suppose LE (d,c,P) & LE (c,a,P) & LE (a,b,P);

            hence thesis by A11, JORDAN6: 57;

          end;

            suppose LE (c,a,P) & LE (a,b,P) & LE (b,d,P);

            hence thesis by A3, A12, JORDAN6: 57;

          end;

        end;

      end;

        suppose

         A13: LE (d,a,P) & LE (a,b,P) & LE (b,c,P);

        then

         A14: LE (d,b,P) by JORDAN6: 58;

        thus thesis

        proof

          per cases by A5;

            suppose LE (a,b,P) & LE (b,d,P) & LE (d,c,P);

            hence thesis by A3, A14, JORDAN6: 57;

          end;

            suppose LE (b,d,P) & LE (d,c,P) & LE (c,a,P);

            hence thesis by A3, A14, JORDAN6: 57;

          end;

            suppose

             A15: LE (d,c,P) & LE (c,a,P) & LE (a,b,P);

             LE (a,c,P) by A13, JORDAN6: 58;

            hence thesis by A2, A15, JORDAN6: 57;

          end;

            suppose LE (c,a,P) & LE (a,b,P) & LE (b,d,P);

            hence thesis by A3, A14, JORDAN6: 57;

          end;

        end;

      end;

    end;

    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

    proof

      assume that

       A1: a in C and

       A2: b in C and

       A3: c in C and

       A4: d in C;

      per cases ;

        suppose LE (a,b,C) & LE (b,c,C) & LE (c,d,C);

        hence thesis;

      end;

        suppose

         A5: LE (a,b,C) & LE (b,c,C) & not LE (c,d,C);

        then

         A6: LE (d,c,C) by A3, A4, JORDAN16: 7;

        thus thesis

        proof

          per cases by A1, A4, JORDAN16: 7;

            suppose

             A7: LE (a,d,C);

             LE (b,d,C) or LE (d,b,C) by A2, A4, JORDAN16: 7;

            hence thesis by A5, A6, A7;

          end;

            suppose LE (d,a,C);

            hence thesis by A5;

          end;

        end;

      end;

        suppose

         A8: LE (a,b,C) & not LE (b,c,C) & LE (c,d,C);

        then

         A9: LE (c,b,C) by A2, A3, JORDAN16: 7;

        thus thesis

        proof

          per cases by A2, A4, JORDAN16: 7;

            suppose

             A10: LE (b,d,C);

             LE (a,c,C) or LE (c,a,C) by A1, A3, JORDAN16: 7;

            hence thesis by A8, A9, A10;

          end;

            suppose

             A11: LE (d,b,C);

            thus thesis

            proof

              per cases by A1, A3, JORDAN16: 7;

                suppose LE (a,c,C);

                hence thesis by A8, A11;

              end;

                suppose

                 A12: LE (c,a,C);

                 LE (a,d,C) or LE (d,a,C) by A1, A4, JORDAN16: 7;

                hence thesis by A8, A11, A12;

              end;

            end;

          end;

        end;

      end;

        suppose

         A13: LE (a,b,C) & not LE (b,c,C) & not LE (c,d,C);

        then

         A14: LE (d,c,C) by A3, A4, JORDAN16: 7;

        

         A15: LE (c,b,C) by A2, A3, A13, JORDAN16: 7;

        thus thesis

        proof

          per cases by A1, A3, JORDAN16: 7;

            suppose

             A16: LE (a,c,C);

             LE (a,d,C) or LE (d,a,C) by A1, A4, JORDAN16: 7;

            hence thesis by A15, A14, A16;

          end;

            suppose LE (c,a,C);

            hence thesis by A13, A14;

          end;

        end;

      end;

        suppose

         A17: not LE (a,b,C) & LE (b,c,C) & LE (c,d,C);

        then

         A18: LE (b,a,C) by A1, A2, JORDAN16: 7;

        thus thesis

        proof

          per cases by A1, A4, JORDAN16: 7;

            suppose

             A19: LE (a,d,C);

             LE (a,c,C) or LE (c,a,C) by A1, A3, JORDAN16: 7;

            hence thesis by A17, A18, A19;

          end;

            suppose LE (d,a,C);

            hence thesis by A17;

          end;

        end;

      end;

        suppose

         A20: not LE (a,b,C) & LE (b,c,C) & not LE (c,d,C);

        then

         A21: LE (b,a,C) & LE (d,c,C) by A1, A2, A3, A4, JORDAN16: 7;

        thus thesis

        proof

          per cases by A1, A4, JORDAN16: 7;

            suppose LE (a,d,C);

            hence thesis by A21;

          end;

            suppose

             A22: LE (d,a,C);

            

             A23: LE (b,d,C) or LE (d,b,C) by A2, A4, JORDAN16: 7;

             LE (a,c,C) or LE (c,a,C) by A1, A3, JORDAN16: 7;

            hence thesis by A20, A21, A22, A23;

          end;

        end;

      end;

        suppose

         A24: not LE (a,b,C) & not LE (b,c,C) & LE (c,d,C);

        then

         A25: LE (b,a,C) & LE (c,b,C) by A1, A2, A3, JORDAN16: 7;

        thus thesis

        proof

          per cases by A1, A4, JORDAN16: 7;

            suppose LE (a,d,C);

            hence thesis by A25;

          end;

            suppose

             A26: LE (d,a,C);

             LE (b,d,C) or LE (d,b,C) by A2, A4, JORDAN16: 7;

            hence thesis by A24, A25, A26;

          end;

        end;

      end;

        suppose

         A27: not LE (a,b,C) & not LE (b,c,C) & not LE (c,d,C);

        then

         A28: LE (d,c,C) by A3, A4, JORDAN16: 7;

         LE (b,a,C) & LE (c,b,C) by A1, A2, A3, A27, JORDAN16: 7;

        hence thesis by A28;

      end;

    end;