pasch.miz



    begin

    reserve OAS for OAffinSpace;

    reserve a,a9,b,b9,c,c9,d,d1,d2,e1,e2,e3,e4,e5,e6,p,p9,q,r,x,y,z for Element of OAS;

    definition

      let OAS;

      :: PASCH:def1

      attr OAS is satisfying_Int_Par_Pasch means for a, b, c, d, p st not (p,b,c) are_collinear & Mid (b,p,a) & (p,c,d) are_collinear & (b,c) '||' (d,a) holds Mid (c,p,d);

    end

    definition

      let OAS;

      :: PASCH:def2

      attr OAS is satisfying_Ext_Par_Pasch means for a, b, c, d, p st Mid (p,b,c) & (p,a,d) are_collinear & (a,b) '||' (c,d) & not (p,a,b) are_collinear holds Mid (p,a,d);

    end

    definition

      let OAS;

      :: PASCH:def3

      attr OAS is satisfying_Gen_Par_Pasch means for a, b, c, a9, b9, c9 st not (a,b,a9) are_collinear & (a,a9) '||' (b,b9) & (a,a9) '||' (c,c9) & Mid (a,b,c) & (a9,b9,c9) are_collinear holds Mid (a9,b9,c9);

    end

    definition

      let OAS;

      :: PASCH:def4

      attr OAS is satisfying_Ext_Bet_Pasch means for a, b, c, d, x, y st Mid (a,b,d) & Mid (b,x,c) & not (a,b,c) are_collinear holds ex y st Mid (a,y,c) & Mid (y,x,d);

    end

    definition

      let OAS;

      :: PASCH:def5

      attr OAS is satisfying_Int_Bet_Pasch means for a, b, c, d, x, y st Mid (a,b,d) & Mid (a,x,c) & not (a,b,c) are_collinear holds ex y st Mid (b,y,c) & Mid (x,y,d);

    end

    definition

      let OAS;

      :: PASCH:def6

      attr OAS is Fanoian means for a, b, c, d st (a,b) // (c,d) & (a,c) // (b,d) & not (a,b,c) are_collinear holds ex x st Mid (a,x,d) & Mid (b,x,c);

    end

    theorem :: PASCH:1

    

     Th1: (b,p) // (p,c) & p <> c & b <> p implies ex d st (a,p) // (p,d) & (a,b) '||' (c,d) & c <> d & p <> d

    proof

      assume that

       A1: (b,p) // (p,c) and

       A2: p <> c and

       A3: b <> p;

       A4:

      now

         A5:

        now

           Mid (b,p,c) by A1, DIRAF:def 3;

          then (b,p,c) are_collinear by DIRAF: 28;

          then

           A6: (p,c,b) are_collinear by DIRAF: 30;

          assume (p,a) // (p,b);

          then

           A7: (a,p) // (b,p) by DIRAF: 2;

          then (a,p) // (p,c) by A1, A3, DIRAF: 3;

          then Mid (a,p,c) by DIRAF:def 3;

          then (a,p,c) are_collinear by DIRAF: 28;

          then (p,c,a) are_collinear by DIRAF: 30;

          then

           A8: (p,c) '||' (a,b) by A6, DIRAF: 34;

          

           A9: (p,c) // (b,p) by A1, DIRAF: 2;

          

           A10: (p,c,c) are_collinear by DIRAF: 31;

          consider d such that

           A11: Mid (p,c,d) and

           A12: c <> d by DIRAF: 13;

          

           A13: p <> d by A11, A12, DIRAF: 8;

          (p,c) // (c,d) by A11, DIRAF:def 3;

          then (p,c) // (p,d) by ANALOAF:def 5;

          then

           A14: (b,p) // (p,d) by A2, A9, ANALOAF:def 5;

          (p,c,d) are_collinear by A11, DIRAF: 28;

          then (p,c) '||' (c,d) by A10, DIRAF: 34;

          then (a,b) '||' (c,d) by A2, A8, DIRAF: 23;

          hence thesis by A3, A7, A12, A13, A14, DIRAF: 3;

        end;

         A15:

        now

          assume (p,a) // (b,p);

          then

           A16: (a,p) // (p,b) by DIRAF: 2;

          then Mid (a,p,b) by DIRAF:def 3;

          then (a,p,b) are_collinear by DIRAF: 28;

          then

           A17: (p,b,a) are_collinear by DIRAF: 30;

           Mid (b,p,c) by A1, DIRAF:def 3;

          then (b,p,c) are_collinear by DIRAF: 28;

          then

           A18: (p,b,c) are_collinear by DIRAF: 30;

          

           A19: (a,b,b) are_collinear by DIRAF: 31;

          

           A20: b <> c by A1, A2, ANALOAF:def 5;

          (p,b,b) are_collinear by DIRAF: 31;

          then (a,b,c) are_collinear by A3, A17, A18, DIRAF: 32;

          hence thesis by A3, A16, A20, A19, DIRAF: 34;

        end;

        assume (a,b,p) are_collinear ;

        then (p,a,b) are_collinear by DIRAF: 30;

        then (p,a) '||' (p,b) by DIRAF:def 5;

        hence thesis by A5, A15, DIRAF:def 4;

      end;

      now

        consider d such that

         A21: (a,p) // (p,d) and

         A22: (a,b) // (c,d) by A1, A3, ANALOAF:def 5;

        assume

         A23: not (a,b,p) are_collinear ;

         A24:

        now

          assume d = p;

          then (p,c) // (b,a) by A22, DIRAF: 2;

          then (b,p) // (b,a) by A1, A2, DIRAF: 3;

          then (b,p) '||' (b,a) by DIRAF:def 4;

          then (b,p,a) are_collinear by DIRAF:def 5;

          hence contradiction by A23, DIRAF: 30;

        end;

         A25:

        now

          assume d = c;

          then (p,d) // (b,p) by A1, DIRAF: 2;

          then (a,p) // (b,p) by A21, A24, DIRAF: 3;

          then (p,a) // (p,b) by DIRAF: 2;

          then (p,a) '||' (p,b) by DIRAF:def 4;

          then (p,a,b) are_collinear by DIRAF:def 5;

          hence contradiction by A23, DIRAF: 30;

        end;

        (a,b) '||' (c,d) by A22, DIRAF:def 4;

        hence thesis by A21, A24, A25;

      end;

      hence thesis by A4;

    end;

    theorem :: PASCH:2

    

     Th2: (p,b) // (p,c) & p <> c & b <> p implies ex d st (p,a) // (p,d) & (a,b) '||' (c,d) & c <> d

    proof

      assume that

       A1: (p,b) // (p,c) and

       A2: p <> c and

       A3: b <> p;

      consider q such that

       A4: Mid (b,p,q) and

       A5: p <> q by DIRAF: 13;

      

       A6: (b,p) // (p,q) by A4, DIRAF:def 3;

      then

      consider r such that

       A7: (a,p) // (p,r) and

       A8: (a,b) '||' (q,r) and

       A9: q <> r and

       A10: r <> p by A3, A5, Th1;

      (b,p) // (c,p) by A1, DIRAF: 2;

      then (p,q) // (c,p) by A3, A6, ANALOAF:def 5;

      then (q,p) // (p,c) by DIRAF: 2;

      then

      consider d such that

       A11: (r,p) // (p,d) and

       A12: (r,q) '||' (c,d) and

       A13: c <> d and d <> p by A2, A5, Th1;

      (p,r) // (d,p) by A11, DIRAF: 2;

      then (a,p) // (d,p) by A7, A10, DIRAF: 3;

      then

       A14: (p,a) // (p,d) by DIRAF: 2;

      (q,r) '||' (c,d) by A12, DIRAF: 22;

      then (a,b) '||' (c,d) by A8, A9, DIRAF: 23;

      hence thesis by A13, A14;

    end;

    theorem :: PASCH:3

    (p,b) '||' (p,c) & p <> b implies ex d st (p,a) '||' (p,d) & (a,b) '||' (c,d)

    proof

      assume that

       A1: (p,b) '||' (p,c) and

       A2: p <> b;

       A3:

      now

        assume

         A4: p <> c;

         A5:

        now

          assume (p,b) // (c,p);

          then (b,p) // (p,c) by DIRAF: 2;

          then

          consider d such that

           A6: (a,p) // (p,d) and

           A7: (a,b) '||' (c,d) and c <> d and d <> p by A2, A4, Th1;

          (p,a) // (d,p) by A6, DIRAF: 2;

          then (p,a) '||' (p,d) by DIRAF:def 4;

          hence thesis by A7;

        end;

        now

          assume (p,b) // (p,c);

          then

          consider d such that

           A8: (p,a) // (p,d) and

           A9: (a,b) '||' (c,d) and c <> d by A2, A4, Th2;

          (p,a) '||' (p,d) by A8, DIRAF:def 4;

          hence thesis by A9;

        end;

        hence thesis by A1, A5, DIRAF:def 4;

      end;

      now

        

         A10: (a,b) '||' (p,p) by DIRAF: 20;

        

         A11: (p,a) '||' (p,p) by DIRAF: 20;

        assume p = c;

        hence thesis by A11, A10;

      end;

      hence thesis by A3;

    end;

    theorem :: PASCH:4

    

     Th4: not (p,a,b) are_collinear & (p,b,c) are_collinear & (p,a,d1) are_collinear & (p,a,d2) are_collinear & (a,b) '||' (c,d1) & (a,b) '||' (c,d2) implies d1 = d2

    proof

      assume that

       A1: not (p,a,b) are_collinear and

       A2: (p,b,c) are_collinear and

       A3: (p,a,d1) are_collinear and

       A4: (p,a,d2) are_collinear and

       A5: (a,b) '||' (c,d1) and

       A6: (a,b) '||' (c,d2);

      

       A7: p <> a by A1, DIRAF: 31;

      

       A8: a <> b by A1, DIRAF: 31;

       A9:

      now

        (p,a,a) are_collinear by DIRAF: 31;

        then

         A10: (d1,d2,a) are_collinear by A3, A4, A7, DIRAF: 32;

        

         A11: (d1,d2,d1) are_collinear by DIRAF: 31;

        

         A12: (p,c,b) are_collinear by A2, DIRAF: 30;

        

         A13: (d1,d2,d2) are_collinear by DIRAF: 31;

        

         A14: (p,a,p) are_collinear by DIRAF: 31;

        then

         A15: (d1,d2,p) are_collinear by A3, A4, A7, DIRAF: 32;

        (c,d1) '||' (c,d2) by A5, A6, A8, DIRAF: 23;

        then

         A16: (c,d1,d2) are_collinear by DIRAF:def 5;

        then

         A17: (d1,d2,c) are_collinear by DIRAF: 30;

        assume

         A18: p <> c;

        assume

         A19: d1 <> d2;

        (d1,d2,p) are_collinear by A3, A4, A7, A14, DIRAF: 32;

        then

         A20: (p,c,d1) are_collinear by A19, A17, A11, DIRAF: 32;

        (d1,d2,c) are_collinear by A16, DIRAF: 30;

        then (p,c,d2) are_collinear by A19, A15, A13, DIRAF: 32;

        then (d1,d2,b) are_collinear by A18, A20, A12, DIRAF: 32;

        hence contradiction by A1, A19, A15, A10, DIRAF: 32;

      end;

      

       A21: (p,d2,a) are_collinear by A4, DIRAF: 30;

      

       A22: (p,d1,a) are_collinear by A3, DIRAF: 30;

      now

        

         A23: (p,d2,p) are_collinear by DIRAF: 31;

        assume

         A24: c = p;

        then

         A25: (p,d2) '||' (a,b) by A6, DIRAF: 22;

         A26:

        now

          assume

           A27: p <> d2;

          then (p,d2,b) are_collinear by A21, A25, DIRAF: 33;

          hence contradiction by A1, A21, A23, A27, DIRAF: 32;

        end;

        

         A28: (p,d1,p) are_collinear by DIRAF: 31;

        

         A29: (p,d1) '||' (a,b) by A5, A24, DIRAF: 22;

        now

          assume

           A30: p <> d1;

          then (p,d1,b) are_collinear by A22, A29, DIRAF: 33;

          hence contradiction by A1, A22, A28, A30, DIRAF: 32;

        end;

        hence thesis by A26;

      end;

      hence thesis by A9;

    end;

    theorem :: PASCH:5

    

     Th5: not (a,b,c) are_collinear & (a,b) '||' (c,d1) & (a,b) '||' (c,d2) & (a,c) '||' (b,d1) & (a,c) '||' (b,d2) implies d1 = d2

    proof

      assume that

       A1: not (a,b,c) are_collinear and

       A2: (a,b) '||' (c,d1) and

       A3: (a,b) '||' (c,d2) and

       A4: (a,c) '||' (b,d1) and

       A5: (a,c) '||' (b,d2);

      assume

       A6: d1 <> d2;

      a <> c by A1, DIRAF: 31;

      then (b,d1) '||' (b,d2) by A4, A5, DIRAF: 23;

      then (b,d1,d2) are_collinear by DIRAF:def 5;

      then

       A7: (d1,d2,b) are_collinear by DIRAF: 30;

       A8:

      now

        assume c = d1;

        then (c,a) '||' (c,b) by A4, DIRAF: 22;

        then (c,a,b) are_collinear by DIRAF:def 5;

        hence contradiction by A1, DIRAF: 30;

      end;

      

       A9: (d1,d2,d1) are_collinear by DIRAF: 31;

      a <> b by A1, DIRAF: 31;

      then (c,d1) '||' (c,d2) by A2, A3, DIRAF: 23;

      then

       A10: (c,d1,d2) are_collinear by DIRAF:def 5;

      then

       A11: (d1,d2,c) are_collinear by DIRAF: 30;

      (d1,d2,c) are_collinear by A10, DIRAF: 30;

      then (d1,d2) '||' (c,d1) by A9, DIRAF: 34;

      then (d1,d2) '||' (a,b) or c = d1 by A2, DIRAF: 23;

      then (d1,d2) '||' (b,a) by A8, DIRAF: 22;

      then (d1,d2,a) are_collinear by A6, A7, DIRAF: 33;

      hence contradiction by A1, A6, A11, A7, DIRAF: 32;

    end;

    theorem :: PASCH:6

    

     Th6: not (p,b,c) are_collinear & Mid (b,p,a) & (p,c,d) are_collinear & (b,c) '||' (d,a) implies Mid (c,p,d)

    proof

      assume that

       A1: not (p,b,c) are_collinear and

       A2: Mid (b,p,a) and

       A3: (p,c,d) are_collinear and

       A4: (b,c) '||' (d,a);

      

       A5: (p,d,c) are_collinear by A3, DIRAF: 30;

      (b,p,a) are_collinear by A2, DIRAF: 28;

      then

       A6: (p,b,a) are_collinear by DIRAF: 30;

      (p,c) '||' (p,d) by A3, DIRAF:def 5;

      then

       A7: (p,c) // (p,d) or (p,c) // (d,p) by DIRAF:def 4;

      assume

       A8: not Mid (c,p,d);

      then

       A9: d <> p by DIRAF: 10;

       A10:

      now

        assume (p,c) // (d,p);

        then (c,p) // (p,d) by DIRAF: 2;

        hence contradiction by A8, DIRAF:def 3;

      end;

      p <> c by A8, DIRAF: 10;

      then

      consider q such that

       A11: (p,b) // (p,q) and

       A12: (b,c) '||' (d,q) and d <> q by A9, A7, A10, Th2;

      

       A13: (p,d,p) are_collinear by DIRAF: 31;

      (p,b) '||' (p,q) by A11, DIRAF:def 4;

      then (p,b,q) are_collinear by DIRAF:def 5;

      then a = q by A1, A3, A4, A12, A6, Th4;

      then (b,p) // (p,q) by A2, DIRAF:def 3;

      then (p,q) // (b,p) by DIRAF: 2;

      then (p,b) // (b,p) or p = q by A11, DIRAF: 3;

      then p = b or p = q by ANALOAF:def 5;

      then (p,d) '||' (c,b) by A1, A12, DIRAF: 22, DIRAF: 31;

      then (p,d,b) are_collinear by A9, A5, DIRAF: 33;

      hence contradiction by A1, A9, A5, A13, DIRAF: 32;

    end;

    theorem :: PASCH:7

    OAS is satisfying_Int_Par_Pasch by Th6;

    theorem :: PASCH:8

    

     Th8: Mid (p,b,c) & (p,a,d) are_collinear & (a,b) '||' (c,d) & not (p,a,b) are_collinear implies Mid (p,a,d)

    proof

      assume that

       A1: Mid (p,b,c) and

       A2: (p,a,d) are_collinear and

       A3: (a,b) '||' (c,d) and

       A4: not (p,a,b) are_collinear ;

       A5:

      now

        (d,a,p) are_collinear by A2, DIRAF: 30;

        then (d,a) '||' (d,p) by DIRAF:def 5;

        then

         A6: (a,d) '||' (d,p) by DIRAF: 22;

        assume

         A7: b <> c;

        

         A8: b <> a by A4, DIRAF: 31;

        

         A9: not (d,b,a) are_collinear

        proof

          assume (d,b,a) are_collinear ;

          then

           A10: (a,b,d) are_collinear by DIRAF: 30;

          (a,b) '||' (d,c) by A3, DIRAF: 22;

          then (a,b,c) are_collinear by A8, A10, DIRAF: 33;

          then

           A11: (b,c,a) are_collinear by DIRAF: 30;

          (p,b,c) are_collinear by A1, DIRAF: 28;

          then

           A12: (b,c,p) are_collinear by DIRAF: 30;

          (b,c,b) are_collinear by DIRAF: 31;

          hence contradiction by A4, A7, A11, A12, DIRAF: 32;

        end;

        then d <> a by DIRAF: 31;

        then

        consider q such that

         A13: (b,d) '||' (d,q) and

         A14: (b,a) '||' (p,q) by A6, DIRAF: 27;

        

         A15: (p,b,c) are_collinear by A1, DIRAF: 28;

        

         A16: p <> c by A1, A7, DIRAF: 8;

        

         A17: not (b,c,d) are_collinear

        proof

          

           A18: (p,c,c) are_collinear by DIRAF: 31;

          (p,b,c) are_collinear by A1, DIRAF: 28;

          then

           A19: (p,c,b) are_collinear by DIRAF: 30;

          assume

           A20: (b,c,d) are_collinear ;

          

           A21: (b,c,b) are_collinear by DIRAF: 31;

           A22:

          now

            assume (a,b) '||' (c,b);

            then (b,c) '||' (b,a) by DIRAF: 22;

            then (b,c,a) are_collinear by DIRAF:def 5;

            hence contradiction by A7, A9, A20, A21, DIRAF: 32;

          end;

          (c,d,b) are_collinear by A20, DIRAF: 30;

          then (c,d) '||' (c,b) by DIRAF:def 5;

          then (p,a,c) are_collinear by A2, A3, A22, DIRAF: 23;

          then (p,c,a) are_collinear by DIRAF: 30;

          then (b,c,a) are_collinear by A16, A19, A18, DIRAF: 32;

          hence contradiction by A7, A9, A20, A21, DIRAF: 32;

        end;

        (a,b) '||' (q,p) by A14, DIRAF: 22;

        then

         A23: (c,d) '||' (q,p) by A3, A8, DIRAF: 23;

        (d,b) '||' (d,q) by A13, DIRAF: 22;

        then (d,b,q) are_collinear by DIRAF:def 5;

        then

         A24: (b,d,q) are_collinear by DIRAF: 30;

        

         A25: d <> p

        proof

          

           A26: (p,c,p) are_collinear by DIRAF: 31;

          (p,b,c) are_collinear by A1, DIRAF: 28;

          then

           A27: (p,c,b) are_collinear by DIRAF: 30;

          assume d = p;

          then (p,c) '||' (b,a) by A3, DIRAF: 22;

          then (p,c,a) are_collinear by A16, A27, DIRAF: 33;

          hence contradiction by A4, A16, A27, A26, DIRAF: 32;

        end;

        

         A28: not (d,p,q) are_collinear

        proof

           A29:

          now

            assume p = q;

            then (d,b) '||' (d,p) by A13, DIRAF: 22;

            then (d,b,p) are_collinear by DIRAF:def 5;

            then

             A30: (d,p,b) are_collinear by DIRAF: 30;

            

             A31: (d,p,d) are_collinear by DIRAF: 31;

            (d,p,a) are_collinear by A2, DIRAF: 30;

            hence contradiction by A9, A25, A31, A30, DIRAF: 32;

          end;

          

           A32: (p,q,p) are_collinear by DIRAF: 31;

          

           A33: (d,p,p) are_collinear by DIRAF: 31;

          assume

           A34: (d,p,q) are_collinear ;

          (d,p,a) are_collinear by A2, DIRAF: 30;

          then

           A35: (p,q,a) are_collinear by A25, A34, A33, DIRAF: 32;

          (p,q) '||' (a,b) by A14, DIRAF: 22;

          then (p,q,b) are_collinear by A35, A29, DIRAF: 33;

          hence contradiction by A4, A35, A29, A32, DIRAF: 32;

        end;

         Mid (c,b,p) by A1, DIRAF: 9;

        then

         A36: Mid (d,b,q) by A17, A24, A23, Th6;

         A37:

        now

          (d,b) '||' (d,q) by A13, DIRAF: 22;

          then (d,b,q) are_collinear by DIRAF:def 5;

          then

           A38: (d,q,b) are_collinear by DIRAF: 30;

          assume

           A39: Mid (p,d,a);

          (p,q) '||' (b,a) by A14, DIRAF: 22;

          then Mid (q,d,b) by A28, A39, A38, Th6;

          then Mid (b,d,q) by DIRAF: 9;

          then b = d by A36, DIRAF: 14;

          hence contradiction by A9, DIRAF: 31;

        end;

        assume not Mid (p,a,d);

        then Mid (a,p,d) by A2, A37, DIRAF: 29;

        then Mid (b,p,c) by A3, A4, A15, Th6;

        then p = b by A1, DIRAF: 14;

        hence contradiction by A4, DIRAF: 31;

      end;

      now

        

         A40: (a,b) '||' (b,a) by DIRAF: 19;

        

         A41: (p,a,a) are_collinear by DIRAF: 31;

        

         A42: (p,b,b) are_collinear by DIRAF: 31;

        assume b = c;

        then a = d by A2, A3, A4, A42, A41, A40, Th4;

        hence thesis by DIRAF: 10;

      end;

      hence thesis by A5;

    end;

    theorem :: PASCH:9

    OAS is satisfying_Ext_Par_Pasch by Th8;

    theorem :: PASCH:10

    

     Th10: not (a,b,a9) are_collinear & (a,a9) '||' (b,b9) & (a,a9) '||' (c,c9) & Mid (a,b,c) & (a9,b9,c9) are_collinear implies Mid (a9,b9,c9)

    proof

      assume that

       A1: not (a,b,a9) are_collinear and

       A2: (a,a9) '||' (b,b9) and

       A3: (a,a9) '||' (c,c9) and

       A4: Mid (a,b,c) and

       A5: (a9,b9,c9) are_collinear ;

      

       A6: (a,b,c) are_collinear by A4, DIRAF: 28;

      

       A7: (b9,c9,a9) are_collinear by A5, DIRAF: 30;

      

       A8: (c9,b9,a9) are_collinear by A5, DIRAF: 30;

      

       A9: a <> a9 by A1, DIRAF: 31;

      then

       A10: (b,b9) '||' (c,c9) by A2, A3, DIRAF: 23;

      

       A11: a <> b by A1, DIRAF: 31;

      then

       A12: a <> c by A4, DIRAF: 8;

       A13:

      now

        assume that

         A14: b9 <> c9 and a9 <> b9 and

         A15: b <> b9;

        

         A16: not (b,b9,a9) are_collinear

        proof

          

           A17: (b,b9,b) are_collinear by DIRAF: 31;

          assume

           A18: (b,b9,a9) are_collinear ;

          (b,b9) '||' (a9,a) by A2, DIRAF: 22;

          then (b,b9,a) are_collinear by A15, A18, DIRAF: 33;

          hence contradiction by A1, A15, A18, A17, DIRAF: 32;

        end;

         A19:

        now

          (a,b) '||' (a,c) by A6, DIRAF:def 5;

          then (c,a) '||' (a,b) by DIRAF: 22;

          then

          consider x such that

           A20: (c9,a) '||' (a,x) and

           A21: (c9,c) '||' (b,x) by A12, DIRAF: 27;

          (a,c9) '||' (a,x) by A20, DIRAF: 22;

          then

           A22: (a,c9,x) are_collinear by DIRAF:def 5;

          assume

           A23: c <> c9;

          

           A24: x <> b

          proof

            assume x = b;

            then

             A25: (a,b,c9) are_collinear by A22, DIRAF: 30;

            (a,b,b) are_collinear by DIRAF: 31;

            then

             A26: (c,c9,b) are_collinear by A11, A6, A25, DIRAF: 32;

            (a,b,a) are_collinear by DIRAF: 31;

            then (c,c9,a) are_collinear by A11, A6, A25, DIRAF: 32;

            then (c,c9) '||' (a,b) by A26, DIRAF: 34;

            then (b,b9) '||' (a,b) by A10, A23, DIRAF: 23;

            then (a,a9) '||' (a,b) by A2, A15, DIRAF: 23;

            then (a,a9,b) are_collinear by DIRAF:def 5;

            hence contradiction by A1, DIRAF: 30;

          end;

          (c,c9) '||' (b,x) by A21, DIRAF: 22;

          then (b,b9) '||' (b,x) by A10, A23, DIRAF: 23;

          then

           A27: (b,b9,x) are_collinear by DIRAF:def 5;

          then (b,x,b9) are_collinear by DIRAF: 30;

          then (b,x) '||' (b,b9) by DIRAF:def 5;

          then (b,x) '||' (c,c9) by A10, A15, DIRAF: 23;

          then

           A28: (x,b) '||' (c,c9) by DIRAF: 22;

          

           A29: x <> b9

          proof

            assume x = b9;

            then

             A30: (b9,c9,a) are_collinear by A22, DIRAF: 30;

            

             A31: (a,a9) '||' (b9,b) by A2, DIRAF: 22;

            (b9,c9,b9) are_collinear by DIRAF: 31;

            then (a,a9,b9) are_collinear by A7, A14, A30, DIRAF: 32;

            then (a,a9,b) are_collinear by A9, A31, DIRAF: 33;

            hence contradiction by A1, DIRAF: 30;

          end;

          

           A32: not (c9,b9,x) are_collinear

          proof

            assume (c9,b9,x) are_collinear ;

            then

             A33: (b9,x,c9) are_collinear by DIRAF: 30;

            

             A34: (b9,x,b9) are_collinear by DIRAF: 31;

            

             A35: (c9,b9,b9) are_collinear by DIRAF: 31;

            (b9,x,b) are_collinear by A27, DIRAF: 30;

            then (c9,b9,b) are_collinear by A29, A33, A34, DIRAF: 32;

            hence contradiction by A8, A14, A16, A35, DIRAF: 32;

          end;

          

           A36: (x,b,b9) are_collinear by A27, DIRAF: 30;

          

           A37: not (a,x,b) are_collinear

          proof

            assume (a,x,b) are_collinear ;

            then

             A38: (x,b,a) are_collinear by DIRAF: 30;

            

             A39: (b,b9) '||' (a,a9) by A2, DIRAF: 22;

            (x,b,b) are_collinear by DIRAF: 31;

            then (b,b9,a) are_collinear by A36, A24, A38, DIRAF: 32;

            hence contradiction by A15, A16, A39, DIRAF: 33;

          end;

          (b9,b,x) are_collinear by A27, DIRAF: 30;

          then (b9,b) '||' (b9,x) by DIRAF:def 5;

          then (b,b9) '||' (b9,x) by DIRAF: 22;

          then

           A40: (b9,x) '||' (a,a9) by A2, A15, DIRAF: 23;

          (a,x,c9) are_collinear by A22, DIRAF: 30;

          then Mid (a,x,c9) by A4, A28, A37, Th8;

          then Mid (c9,x,a) by DIRAF: 9;

          then Mid (c9,b9,a9) by A8, A40, A32, Th8;

          hence thesis by DIRAF: 9;

        end;

        c = c9 implies thesis

        proof

          

           A41: not (c9,b9,b) are_collinear

          proof

            

             A42: (c9,b9,b9) are_collinear by DIRAF: 31;

            assume (c9,b9,b) are_collinear ;

            hence contradiction by A8, A14, A16, A42, DIRAF: 32;

          end;

          assume c = c9;

          then

           A43: Mid (c9,b,a) by A4, DIRAF: 9;

          (b9,b) '||' (a,a9) by A2, DIRAF: 22;

          then Mid (c9,b9,a9) by A8, A43, A41, Th8;

          hence thesis by DIRAF: 9;

        end;

        hence thesis by A19;

      end;

      b = b9 implies thesis

      proof

        

         A44: (a,a9) '||' (c9,c) by A3, DIRAF: 22;

        

         A45: (b9,a9,c9) are_collinear by A5, DIRAF: 30;

        assume

         A46: b = b9;

        then not (b9,a,a9) are_collinear by A1, DIRAF: 30;

        hence thesis by A4, A46, A45, A44, Th6;

      end;

      hence thesis by A13, DIRAF: 10;

    end;

    theorem :: PASCH:11

    OAS is satisfying_Gen_Par_Pasch by Th10;

    theorem :: PASCH:12

     not (p,a,b) are_collinear & (a,p) // (p,a9) & (b,p) // (p,b9) & (a,b) '||' (a9,b9) implies (a,b) // (b9,a9)

    proof

      assume that

       A1: not (p,a,b) are_collinear and

       A2: (a,p) // (p,a9) and

       A3: (b,p) // (p,b9) and

       A4: (a,b) '||' (a9,b9);

      

       A5: not (p,b,a) are_collinear by A1, DIRAF: 30;

       Mid (b,p,b9) by A3, DIRAF:def 3;

      then (b,p,b9) are_collinear by DIRAF: 28;

      then

       A6: (p,b,b9) are_collinear by DIRAF: 30;

       Mid (a,p,a9) by A2, DIRAF:def 3;

      then (a,p,a9) are_collinear by DIRAF: 28;

      then

       A7: (p,a,a9) are_collinear by DIRAF: 30;

      

       A8: (b,a) '||' (a9,b9) by A4, DIRAF: 22;

      a <> p by A1, DIRAF: 31;

      then

      consider q such that

       A9: (b,p) // (p,q) and

       A10: (b,a) // (a9,q) by A2, ANALOAF:def 5;

       Mid (b,p,q) by A9, DIRAF:def 3;

      then (b,p,q) are_collinear by DIRAF: 28;

      then

       A11: (p,b,q) are_collinear by DIRAF: 30;

      (b,a) '||' (a9,q) by A10, DIRAF:def 4;

      then (b,a) // (a9,b9) by A10, A5, A7, A6, A11, A8, Th4;

      hence thesis by DIRAF: 2;

    end;

    theorem :: PASCH:13

     not (p,a,a9) are_collinear & (p,a) // (p,b) & (p,a9) // (p,b9) & (a,a9) '||' (b,b9) implies (a,a9) // (b,b9)

    proof

      assume that

       A1: not (p,a,a9) are_collinear and

       A2: (p,a) // (p,b) and

       A3: (p,a9) // (p,b9) and

       A4: (a,a9) '||' (b,b9);

      consider c such that

       A5: Mid (a,p,c) and

       A6: p <> c by DIRAF: 13;

      

       A7: (a,p) // (p,c) by A5, DIRAF:def 3;

      

       A8: a <> p by A1, DIRAF: 31;

      then

      consider c9 such that

       A9: (a9,p) // (p,c9) and

       A10: (a9,a) // (c,c9) by A7, ANALOAF:def 5;

      

       A11: (a9,a) '||' (c9,c) by A10, DIRAF:def 4;

      

       A12: c <> c9

      proof

        assume c = c9;

        then Mid (a9,p,c) by A9, DIRAF:def 3;

        then (a9,p,c) are_collinear by DIRAF: 28;

        then

         A13: (p,c,a9) are_collinear by DIRAF: 30;

        (a,p,c) are_collinear by A5, DIRAF: 28;

        then

         A14: (p,c,a) are_collinear by DIRAF: 30;

        (p,c,p) are_collinear by DIRAF: 31;

        hence contradiction by A1, A6, A14, A13, DIRAF: 32;

      end;

      (p,a) // (c,p) by A7, DIRAF: 2;

      then (c,p) // (p,b) by A2, A8, ANALOAF:def 5;

      then

      consider b99 be Element of OAS such that

       A15: (c9,p) // (p,b99) and

       A16: (c9,c) // (b,b99) by A6, ANALOAF:def 5;

      

       A17: (a9,a) '||' (b,b9) by A4, DIRAF: 22;

      

       A18: p <> c9

      proof

        assume p = c9;

        then (a9,a) '||' (c,p) by A10, DIRAF:def 4;

        then

         A19: (p,c) '||' (a,a9) by DIRAF: 22;

        (a,p) '||' (p,c) by A7, DIRAF:def 4;

        then (a,p) '||' (a,a9) by A6, A19, DIRAF: 23;

        then (a,p,a9) are_collinear by DIRAF:def 5;

        hence contradiction by A1, DIRAF: 30;

      end;

      (p,a) '||' (p,b) by A2, DIRAF:def 4;

      then

       A20: (p,a,b) are_collinear by DIRAF:def 5;

      

       A21: (c9,c) // (a,a9) by A10, DIRAF: 2;

      (a9,p) '||' (p,c9) by A9, DIRAF:def 4;

      then

       A22: (p,a9) '||' (p,c9) by DIRAF: 22;

      (p,a9) '||' (p,b9) by A3, DIRAF:def 4;

      then

       A23: (p,a9,b9) are_collinear by DIRAF:def 5;

      (c9,p) '||' (p,b99) by A15, DIRAF:def 4;

      then (p,c9) '||' (p,b99) by DIRAF: 22;

      then (p,a9) '||' (p,b99) by A18, A22, DIRAF: 23;

      then

       A24: (p,a9,b99) are_collinear by DIRAF:def 5;

      (c9,c) '||' (b,b99) by A16, DIRAF:def 4;

      then

       A25: (a9,a) '||' (b,b99) by A12, A11, DIRAF: 23;

       not (p,a9,a) are_collinear by A1, DIRAF: 30;

      then (c9,c) // (b,b9) by A20, A23, A17, A16, A24, A25, Th4;

      hence thesis by A12, A21, ANALOAF:def 5;

    end;

    theorem :: PASCH:14

    

     Th14: not (p,a,b) are_collinear & (p,a) '||' (b,c) & (p,b) '||' (a,c) implies (p,a) // (b,c) & (p,b) // (a,c)

    proof

      assume that

       A1: not (p,a,b) are_collinear and

       A2: (p,a) '||' (b,c) and

       A3: (p,b) '||' (a,c);

      consider d such that

       A4: (p,a) // (b,d) and

       A5: (p,b) // (a,d) and a <> d by ANALOAF:def 5;

      

       A6: (p,b) '||' (a,d) by A5, DIRAF:def 4;

      (p,a) '||' (b,d) by A4, DIRAF:def 4;

      hence thesis by A1, A2, A3, A4, A5, A6, Th5;

    end;

    theorem :: PASCH:15

    

     Th15: Mid (p,c,b) & (c,d) // (b,a) & (p,d) // (p,a) & not (p,a,b) are_collinear & p <> c implies Mid (p,d,a)

    proof

      assume that

       A1: Mid (p,c,b) and

       A2: (c,d) // (b,a) and

       A3: (p,d) // (p,a) and

       A4: not (p,a,b) are_collinear and

       A5: p <> c;

      

       A6: (p,c,b) are_collinear by A1, DIRAF: 28;

      now

        assume

         A7: Mid (p,a,d);

         A8:

        now

          

           A9: p <> a by A4, DIRAF: 31;

          assume that

           A10: b <> c and

           A11: d <> a;

          assume not Mid (p,d,a);

          then Mid (p,a,d) by A3, DIRAF: 7;

          then (p,a) // (a,d) by DIRAF:def 3;

          then

          consider e1 such that

           A12: (c,a) // (a,e1) and

           A13: (c,p) // (d,e1) by A9, ANALOAF:def 5;

          

           A14: (d,e1) // (c,p) by A13, DIRAF: 2;

          

           A15: c <> e1 by A12, DIRAF:def 3, A4, A6, DIRAF: 8;

           Mid (b,c,p) by A1, DIRAF: 9;

          then

           A16: (b,c) // (c,p) by DIRAF:def 3;

          then

           A17: (c,p) // (b,c) by DIRAF: 2;

          consider e2 such that

           A18: (b,a) // (a,e2) and

           A19: (b,c) // (e1,e2) by A4, A6, A12, ANALOAF:def 5;

          consider e3 such that

           A20: (b,c) // (e2,e3) and

           A21: (b,e2) // (c,e3) and c <> e3 by ANALOAF:def 5;

          

           A22: a <> b by A4, DIRAF: 31;

          

           A23: Mid (c,a,e1) by A12, DIRAF:def 3;

          

           A24: d <> e1

          proof

             Mid (p,d,a) or Mid (p,a,d) by A3, DIRAF: 7;

            then (p,d,a) are_collinear or (p,a,d) are_collinear by DIRAF: 28;

            then

             A25: (d,a,p) are_collinear by DIRAF: 30;

            

             A26: (d,a,a) are_collinear by DIRAF: 31;

            assume d = e1;

            then (c,a,d) are_collinear by A23, DIRAF: 28;

            then (d,a,c) are_collinear by DIRAF: 30;

            then (d,a,b) are_collinear by A5, A6, A25, DIRAF: 35;

            hence contradiction by A4, A11, A25, A26, DIRAF: 32;

          end;

          (b,a) // (b,e2) by A18, ANALOAF:def 5;

          then

           A27: (c,d) // (b,e2) by A2, A22, DIRAF: 3;

          b <> e2 by A22, A18, ANALOAF:def 5;

          then (c,d) // (c,e3) by A21, A27, DIRAF: 3;

          then Mid (c,d,e3) or Mid (c,e3,d) by DIRAF: 7;

          then (c,d,e3) are_collinear or (c,e3,d) are_collinear by DIRAF: 28;

          then

           A28: (d,e3,c) are_collinear by DIRAF: 30;

          (e1,e2) // (c,p) by A10, A19, A16, ANALOAF:def 5;

          then

           A29: (e1,e2) // (d,e1) by A5, A13, DIRAF: 3;

          then (d,e1) // (e1,e2) by DIRAF: 2;

          then

           A30: (d,e1) // (d,e2) by ANALOAF:def 5;

          then (d,e2) // (d,e1) by DIRAF: 2;

          then (d,e2) // (c,p) by A24, A14, DIRAF: 3;

          then (d,e2) // (b,c) by A5, A17, DIRAF: 3;

          then

           A31: (d,e2) // (e2,e3) by A10, A20, DIRAF: 3;

          then Mid (d,e2,e3) by DIRAF:def 3;

          then (d,e2,e3) are_collinear by DIRAF: 28;

          then

           A32: (d,e3,e2) are_collinear by DIRAF: 30;

          

           A33: d <> e2 by A24, A29, ANALOAF:def 5;

          then

           A34: d <> e3 by A31, ANALOAF:def 5;

          (d,e2) // (d,e3) by A31, ANALOAF:def 5;

          then (d,e1) // (d,e3) by A30, A33, DIRAF: 3;

          then Mid (d,e1,e3) or Mid (d,e3,e1) by DIRAF: 7;

          then (d,e1,e3) are_collinear or (d,e3,e1) are_collinear by DIRAF: 28;

          then

           A35: (d,e3,e1) are_collinear by DIRAF: 30;

          (c,a,e1) are_collinear by A23, DIRAF: 28;

          then (c,e1,a) are_collinear by DIRAF: 30;

          then

           A36: (d,e3,a) are_collinear by A15, A28, A35, DIRAF: 35;

          

           A37: a <> e1

          proof

            (p,a) // (a,d) by A7, DIRAF:def 3;

            then

             A38: (d,a) // (a,p) by DIRAF: 2;

            assume a = e1;

            then (c,p) // (a,p) by A11, A13, A38, DIRAF: 3;

            then (p,c) // (p,a) by DIRAF: 2;

            then Mid (p,c,a) or Mid (p,a,c) by DIRAF: 7;

            then (p,c,a) are_collinear or (p,a,c) are_collinear by DIRAF: 28;

            then

             A39: (p,c,a) are_collinear by DIRAF: 30;

            (p,c,p) are_collinear by DIRAF: 31;

            hence contradiction by A4, A5, A6, A39, DIRAF: 32;

          end;

          

           A40: a <> e2

          proof

            assume

             A41: a = e2;

            (e1,a) // (a,c) by A12, DIRAF: 2;

            then (b,c) // (a,c) by A19, A37, A41, DIRAF: 3;

            then (c,b) // (c,a) by DIRAF: 2;

            then Mid (c,b,a) or Mid (c,a,b) by DIRAF: 7;

            then (c,b,a) are_collinear or (c,a,b) are_collinear by DIRAF: 28;

            then

             A42: (c,b,a) are_collinear by DIRAF: 30;

            

             A43: (c,b,b) are_collinear by DIRAF: 31;

            (c,b,p) are_collinear by A6, DIRAF: 30;

            hence contradiction by A4, A10, A42, A43, DIRAF: 32;

          end;

           Mid (b,a,e2) by A18, DIRAF:def 3;

          then (b,a,e2) are_collinear by DIRAF: 28;

          then (a,e2,b) are_collinear by DIRAF: 30;

          then

           A44: (d,e3,b) are_collinear by A40, A36, A32, DIRAF: 35;

          (c,b,p) are_collinear by A6, DIRAF: 30;

          then (d,e3,p) are_collinear by A10, A28, A44, DIRAF: 35;

          hence contradiction by A4, A34, A36, A44, DIRAF: 32;

        end;

        

         A45: (p,a,d) are_collinear by A7, DIRAF: 28;

        now

          assume b = c;

          then Mid (b,d,a) or Mid (b,a,d) by A2, DIRAF: 7;

          then (b,d,a) are_collinear or (b,a,d) are_collinear by DIRAF: 28;

          then

           A46: (d,a,b) are_collinear by DIRAF: 30;

          

           A47: (d,a,a) are_collinear by DIRAF: 31;

          (d,a,p) are_collinear by A45, DIRAF: 30;

          hence a = d by A4, A46, A47, DIRAF: 32;

        end;

        hence thesis by A8, DIRAF: 10;

      end;

      hence thesis by A3, DIRAF: 7;

    end;

    theorem :: PASCH:16

    

     Th16: Mid (p,d,a) & (c,d) // (b,a) & (p,c) // (p,b) & not (p,a,b) are_collinear & p <> c implies Mid (p,c,b)

    proof

      assume that

       A1: Mid (p,d,a) and

       A2: (c,d) // (b,a) and

       A3: (p,c) // (p,b) and

       A4: not (p,a,b) are_collinear and

       A5: p <> c;

      

       A6: p <> d

      proof

        assume

         A7: p = d;

        (c,p) // (b,p) by A3, DIRAF: 2;

        then (b,p) // (b,a) by A2, A5, A7, ANALOAF:def 5;

        then Mid (b,p,a) or Mid (b,a,p) by DIRAF: 7;

        then (b,p,a) are_collinear or (b,a,p) are_collinear by DIRAF: 28;

        hence contradiction by A4, DIRAF: 30;

      end;

       Mid (p,c,b) or Mid (p,b,c) by A3, DIRAF: 7;

      then

       A8: (p,c,b) are_collinear or (p,b,c) are_collinear by DIRAF: 28;

      then

       A9: (p,c,b) are_collinear by DIRAF: 30;

      now

        

         A10: not (p,d,c) are_collinear

        proof

          assume (p,d,c) are_collinear ;

          then

           A11: (p,c,d) are_collinear by DIRAF: 30;

          (p,c,p) are_collinear by DIRAF: 31;

          then

           A12: (p,d,b) are_collinear by A5, A9, A11, DIRAF: 32;

          

           A13: (p,d,p) are_collinear by DIRAF: 31;

          (p,d,a) are_collinear by A1, DIRAF: 28;

          hence contradiction by A4, A6, A12, A13, DIRAF: 32;

        end;

        assume

         A14: Mid (p,b,c);

        (p,d) // (d,a) by A1, DIRAF:def 3;

        then (p,d) // (p,a) by ANALOAF:def 5;

        then

         A15: (p,a) // (p,d) by DIRAF: 2;

        

         A16: p <> b by A4, DIRAF: 31;

        (b,a) // (c,d) by A2, DIRAF: 2;

        then Mid (p,a,d) by A14, A15, A16, A10, Th15;

        then

         A17: Mid (d,a,p) by DIRAF: 9;

         Mid (a,d,p) by A1, DIRAF: 9;

        then (c,a) // (b,a) by A2, A17, DIRAF: 14;

        then (a,c) // (a,b) by DIRAF: 2;

        then Mid (a,c,b) or Mid (a,b,c) by DIRAF: 7;

        then (a,c,b) are_collinear or (a,b,c) are_collinear by DIRAF: 28;

        then

         A18: (b,c,a) are_collinear by DIRAF: 30;

        

         A19: (b,c,b) are_collinear by DIRAF: 31;

        (b,c,p) are_collinear by A8, DIRAF: 30;

        then b = c by A4, A18, A19, DIRAF: 32;

        hence thesis by DIRAF: 10;

      end;

      hence thesis by A3, DIRAF: 7;

    end;

    theorem :: PASCH:17

    

     Th17: not (p,a,b) are_collinear & (p,b) // (p,c) & (b,a) // (c,d) & p <> d implies not Mid (a,p,d)

    proof

      assume that

       A1: not (p,a,b) are_collinear and

       A2: (p,b) // (p,c) and

       A3: (b,a) // (c,d) and

       A4: p <> d;

      assume Mid (a,p,d);

      then Mid (d,p,a) by DIRAF: 9;

      then

       A5: (d,p) // (p,a) by DIRAF:def 3;

      then

       A6: (p,d) // (a,p) by DIRAF: 2;

      consider b9 such that

       A7: (c,p) // (p,b9) and

       A8: (c,d) // (a,b9) by A4, A5, ANALOAF:def 5;

      

       A9: p <> c

      proof

        assume p = c;

        then (b,a) // (a,p) by A3, A4, A6, DIRAF: 3;

        then Mid (b,a,p) by DIRAF:def 3;

        hence contradiction by A1, DIRAF: 9, DIRAF: 28;

      end;

      

       A10: a <> b9

      proof

        assume

         A11: a = b9;

        (b,p) // (c,p) by A2, DIRAF: 2;

        then (b,p) // (p,a) by A9, A7, A11, DIRAF: 3;

        then Mid (b,p,a) by DIRAF:def 3;

        then (b,p,a) are_collinear by DIRAF: 28;

        hence contradiction by A1, DIRAF: 30;

      end;

      (p,c) // (b9,p) by A7, DIRAF: 2;

      then (p,b) // (b9,p) by A2, A9, DIRAF: 3;

      then

       A12: (b9,p) // (p,b) by DIRAF: 2;

      

       A13: c <> d

      proof

        assume c = d;

        then (p,b) // (a,p) by A2, A4, A6, DIRAF: 3;

        then (b,p) // (p,a) by DIRAF: 2;

        then Mid (b,p,a) by DIRAF:def 3;

        then (b,p,a) are_collinear by DIRAF: 28;

        hence contradiction by A1, DIRAF: 30;

      end;

      p <> b9

      proof

        assume p = b9;

        then (b,a) // (a,p) by A3, A13, A8, DIRAF: 3;

        then Mid (b,a,p) by DIRAF:def 3;

        hence contradiction by A1, DIRAF: 9, DIRAF: 28;

      end;

      then

      consider b99 be Element of OAS such that

       A14: (a,p) // (p,b99) and

       A15: (a,b9) // (b,b99) by A12, ANALOAF:def 5;

      a <> p by A1, DIRAF: 31;

      then

       A16: a <> b99 by A14, ANALOAF:def 5;

      (b,a) // (a,b9) by A3, A13, A8, DIRAF: 3;

      then (b,a) // (b,b99) by A15, A10, DIRAF: 3;

      then Mid (b,a,b99) or Mid (b,b99,a) by DIRAF: 7;

      then (b,a,b99) are_collinear or (b,b99,a) are_collinear by DIRAF: 28;

      then

       A17: (a,b99,b) are_collinear by DIRAF: 30;

       Mid (a,p,b99) by A14, DIRAF:def 3;

      then (a,p,b99) are_collinear by DIRAF: 28;

      then

       A18: (a,b99,p) are_collinear by DIRAF: 30;

      (a,b99,a) are_collinear by DIRAF: 31;

      hence contradiction by A1, A18, A16, A17, DIRAF: 32;

    end;

    theorem :: PASCH:18

    

     Th18: (p,b) // (p,c) & b <> p implies ex x st (p,a) // (p,x) & (b,a) // (c,x)

    proof

      assume that

       A1: (p,b) // (p,c) and

       A2: b <> p;

      

       A3: (b,p) // (c,p) by A1, DIRAF: 2;

       A4:

      now

        assume that p <> c and

         A5: p <> a;

        consider e1 such that

         A6: Mid (a,p,e1) and

         A7: p <> e1 by DIRAF: 13;

        (a,p) // (p,e1) by A6, DIRAF:def 3;

        then

        consider e2 such that

         A8: (b,p) // (p,e2) and

         A9: (b,a) // (e1,e2) by A5, ANALOAF:def 5;

         Mid (e1,p,a) by A6, DIRAF: 9;

        then

         A10: (e1,p) // (p,a) by DIRAF:def 3;

         A11:

        now

           A12:

          now

             A13:

            now

              assume (b,p) // (a,p);

              then (a,p) // (c,p) by A2, A3, ANALOAF:def 5;

              hence (p,a) // (p,c) & (b,a) // (c,c) by DIRAF: 2, DIRAF: 4;

            end;

            assume

             A14: (a,b) // (b,p);

            then (a,b) // (a,p) by ANALOAF:def 5;

            then (b,p) // (a,p) or a = b by A14, ANALOAF:def 5;

            hence thesis by A13, DIRAF: 1;

          end;

           A15:

          now

            assume

             A16: (a,p) // (p,b);

            then (a,p) // (a,b) by ANALOAF:def 5;

            then (a,b) // (p,b) by A5, A16, ANALOAF:def 5;

            then (b,a) // (b,p) by DIRAF: 2;

            hence (p,a) // (p,p) & (b,a) // (c,p) by A2, A3, DIRAF: 3, DIRAF: 4;

          end;

          assume p = e2;

          then (b,a) // (p,a) by A7, A10, A9, DIRAF: 3;

          then (a,b) // (a,p) by DIRAF: 2;

          hence thesis by A12, A15, DIRAF: 6;

        end;

         A17:

        now

           A18:

          now

            assume that (p,a) // (a,b) and

             A19: (p,c) // (c,a);

            (p,c) // (p,a) by A19, ANALOAF:def 5;

            hence (p,a) // (p,c) & (b,a) // (c,c) by DIRAF: 2, DIRAF: 4;

          end;

           A20:

          now

            assume that (p,b) // (b,a) and

             A21: (p,c) // (c,a);

            (p,c) // (p,a) by A21, ANALOAF:def 5;

            hence (p,a) // (p,c) & (b,a) // (c,c) by DIRAF: 2, DIRAF: 4;

          end;

           A22:

          now

            assume that

             A23: (p,a) // (a,b) and

             A24: (p,a) // (a,c);

            (a,b) // (a,c) by A5, A23, A24, ANALOAF:def 5;

            hence (p,a) // (p,a) & (b,a) // (c,a) by DIRAF: 1, DIRAF: 2;

          end;

          

           A25: (p,b) // (b,a) & (p,a) // (a,c) implies (p,a) // (p,c) & (b,a) // (c,c) by ANALOAF:def 5;

          assume that

           A26: e1 = e2 and

           A27: e2 <> p;

          (p,e2) // (a,p) by A10, A26, DIRAF: 2;

          then (b,p) // (a,p) by A8, A27, DIRAF: 3;

          then

           A28: (p,b) // (p,a) by DIRAF: 2;

          then (p,a) // (p,c) by A1, A2, ANALOAF:def 5;

          hence thesis by A28, A25, A20, A22, A18, DIRAF: 6;

        end;

        now

          assume that

           A29: e1 <> e2 and

           A30: e2 <> p;

          (p,b) // (e2,p) by A8, DIRAF: 2;

          then (e2,p) // (p,c) by A1, A2, ANALOAF:def 5;

          then

          consider x such that

           A31: (e1,p) // (p,x) and

           A32: (e1,e2) // (c,x) by A30, ANALOAF:def 5;

          

           A33: (p,a) // (p,x) by A7, A10, A31, ANALOAF:def 5;

          (b,a) // (c,x) by A9, A29, A32, DIRAF: 3;

          hence thesis by A33;

        end;

        hence thesis by A17, A11;

      end;

      

       A34: p = c implies (p,a) // (p,c) & (b,a) // (c,c) by DIRAF: 4;

      p = a implies (p,a) // (p,a) & (b,a) // (c,a) by A1, DIRAF: 1, DIRAF: 2;

      hence thesis by A34, A4;

    end;

    theorem :: PASCH:19

    

     Th19: Mid (p,c,b) implies ex x st Mid (p,x,a) & (b,a) // (c,x)

    proof

      

       A1: b = c implies Mid (p,a,a) & (b,a) // (c,a) by DIRAF: 1, DIRAF: 10;

      assume

       A2: Mid (p,c,b);

       A3:

      now

        assume p = b;

        then p = c by A2, DIRAF: 8;

        hence Mid (p,p,a) & (b,a) // (c,p) by DIRAF: 4, DIRAF: 10;

      end;

      

       A4: (p,c) // (c,b) by A2, DIRAF:def 3;

       A5:

      now

        assume that

         A6: p <> c and

         A7: p <> b and

         A8: b <> c;

         Mid (b,c,p) by A2, DIRAF: 9;

        then

         A9: (b,c) // (c,p) by DIRAF:def 3;

        then

         A10: (b,c) // (b,p) by ANALOAF:def 5;

        then

         A11: (b,p) // (c,p) by A8, A9, ANALOAF:def 5;

         A12:

        now

           A13:

          now

            assume

             A14: Mid (p,a,b);

             A15:

            now

               Mid (b,a,p) by A14, DIRAF: 9;

              then (b,a) // (a,p) by DIRAF:def 3;

              then

               A16: (a,p) // (b,a) by DIRAF: 2;

              assume Mid (p,a,c);

              then Mid (c,a,p) by DIRAF: 9;

              then (c,a) // (a,p) by DIRAF:def 3;

              then

               A17: (a,p) // (c,a) by DIRAF: 2;

              

               A18: (b,a) // (c,a) implies Mid (p,a,a) & (b,a) // (c,a) by DIRAF: 10;

              a = p implies Mid (p,p,a) & (b,a) // (c,p) by A8, A9, A10, ANALOAF:def 5, DIRAF: 10;

              hence thesis by A17, A16, A18, ANALOAF:def 5;

            end;

             Mid (p,c,a) implies Mid (p,c,a) & (b,a) // (c,c) by DIRAF: 4;

            hence thesis by A2, A14, A15, DIRAF: 17;

          end;

           A19:

          now

            assume Mid (a,p,b);

            then Mid (b,p,a) by DIRAF: 9;

            then (b,p) // (p,a) by DIRAF:def 3;

            then (b,p) // (b,a) by ANALOAF:def 5;

            hence Mid (p,p,a) & (b,a) // (c,p) by A7, A11, ANALOAF:def 5, DIRAF: 10;

          end;

           A20:

          now

            

             A21: (p,c) // (p,b) by A4, ANALOAF:def 5;

            assume

             A22: Mid (p,b,a);

            then (p,b) // (b,a) by DIRAF:def 3;

            then (p,c) // (b,a) by A7, A21, DIRAF: 3;

            then (b,a) // (c,b) by A4, A6, ANALOAF:def 5;

            hence thesis by A22;

          end;

          assume (p,a,b) are_collinear ;

          hence thesis by A13, A19, A20, DIRAF: 29;

        end;

        now

          

           A23: (p,b) // (p,c) by A2, DIRAF: 7;

          assume

           A24: not (p,a,b) are_collinear ;

          then p <> b by DIRAF: 31;

          then

          consider x such that

           A25: (p,a) // (p,x) and

           A26: (b,a) // (c,x) by A23, Th18;

          

           A27: (p,x) // (p,a) by A25, DIRAF: 2;

          (c,x) // (b,a) by A26, DIRAF: 2;

          hence thesis by A2, A6, A24, A26, A27, Th15;

        end;

        hence thesis by A12;

      end;

      p = c implies Mid (p,p,a) & (b,a) // (c,p) by DIRAF: 4, DIRAF: 10;

      hence thesis by A3, A1, A5;

    end;

    theorem :: PASCH:20

    

     Th20: p <> b & Mid (p,b,c) implies ex x st Mid (p,a,x) & (b,a) // (c,x)

    proof

      assume that

       A1: p <> b and

       A2: Mid (p,b,c);

      

       A3: (p,b) // (b,c) by A2, DIRAF:def 3;

      then

       A4: (p,b) // (p,c) by ANALOAF:def 5;

       A5:

      now

        assume

         A6: not (p,a,b) are_collinear ;

        consider x such that

         A7: (p,a) // (p,x) and

         A8: (b,a) // (c,x) by A1, A4, Th18;

        

         A9: p <> c by A1, A2, DIRAF: 8;

        

         A10: p <> x

        proof

          (p,b) // (p,c) by A2, DIRAF: 7;

          then

           A11: (c,p) // (b,p) by DIRAF: 2;

          assume p = x;

          then (b,a) // (b,p) by A8, A9, A11, DIRAF: 3;

          then Mid (b,a,p) or Mid (b,p,a) by DIRAF: 7;

          then (b,a,p) are_collinear or (b,p,a) are_collinear by DIRAF: 28;

          hence contradiction by A6, DIRAF: 30;

        end;

         not (p,x,c) are_collinear

        proof

           Mid (p,a,x) or Mid (p,x,a) by A7, DIRAF: 7;

          then (p,a,x) are_collinear or (p,x,a) are_collinear by DIRAF: 28;

          then

           A12: (p,x,a) are_collinear by DIRAF: 30;

          

           A13: (p,x,p) are_collinear by DIRAF: 31;

          (p,b,c) are_collinear by A2, DIRAF: 28;

          then

           A14: (p,c,b) are_collinear by DIRAF: 30;

          

           A15: (p,c,p) are_collinear by DIRAF: 31;

          assume (p,x,c) are_collinear ;

          then (p,c,a) are_collinear by A10, A12, A13, DIRAF: 32;

          hence contradiction by A6, A9, A14, A15, DIRAF: 32;

        end;

        hence thesis by A1, A2, A7, A8, Th15;

      end;

       A16:

      now

        assume that

         A17: (p,a,b) are_collinear and

         A18: c <> b;

         A19:

        now

          assume Mid (p,a,b);

          then Mid (a,b,c) by A2, DIRAF: 11;

          then Mid (c,b,a) by DIRAF: 9;

          then

           A20: (c,b) // (b,a) by DIRAF:def 3;

          then (c,b) // (c,a) by ANALOAF:def 5;

          hence Mid (p,a,a) & (b,a) // (c,a) by A18, A20, ANALOAF:def 5, DIRAF: 10;

        end;

         A21:

        now

          assume Mid (p,b,a);

          then

           A22: (p,b) // (b,a) by DIRAF:def 3;

           A23:

          now

             A24:

            now

              assume (p,a) // (a,c);

              then Mid (p,a,c) by DIRAF:def 3;

              hence thesis by DIRAF: 4;

            end;

             A25:

            now

              assume a = b;

              then (b,a) // (c,a) by DIRAF: 4;

              hence thesis by DIRAF: 10;

            end;

            (p,b) // (p,a) by A22, ANALOAF:def 5;

            then

             A26: (b,a) // (p,a) by A1, A22, ANALOAF:def 5;

            assume (b,a) // (a,c);

            hence thesis by A26, A25, A24, ANALOAF:def 5;

          end;

           A27:

          now

            assume

             A28: (b,c) // (c,a);

            then (b,c) // (b,a) by ANALOAF:def 5;

            hence Mid (p,a,a) & (b,a) // (c,a) by A18, A28, ANALOAF:def 5, DIRAF: 10;

          end;

          (b,a) // (b,c) by A1, A3, A22, ANALOAF:def 5;

          hence thesis by A23, A27, ANALOAF:def 5;

        end;

        now

          assume Mid (a,p,b);

          then Mid (a,b,c) by A1, A2, DIRAF: 12;

          then Mid (c,b,a) by DIRAF: 9;

          then

           A29: (c,b) // (b,a) by DIRAF:def 3;

          then (c,b) // (c,a) by ANALOAF:def 5;

          hence Mid (p,a,a) & (b,a) // (c,a) by A18, A29, ANALOAF:def 5, DIRAF: 10;

        end;

        hence thesis by A17, A19, A21, DIRAF: 29;

      end;

      c = b implies Mid (p,a,a) & (b,a) // (c,a) by DIRAF: 1, DIRAF: 10;

      hence thesis by A5, A16;

    end;

    theorem :: PASCH:21

    

     Th21: not (p,a,b) are_collinear & Mid (p,c,b) implies ex x st Mid (p,x,a) & (a,b) // (x,c)

    proof

      assume that

       A1: not (p,a,b) are_collinear and

       A2: Mid (p,c,b);

      

       A3: p <> a by A1, DIRAF: 31;

      

       A4: (p,c,b) are_collinear by A2, DIRAF: 28;

      

       A5: Mid (b,c,p) by A2, DIRAF: 9;

      then

       A6: (b,c) // (c,p) by DIRAF:def 3;

      

       A7: a <> b by A1, DIRAF: 31;

       A8:

      now

        assume that

         A9: b <> c and

         A10: a <> c and

         A11: p <> c;

        consider e1 such that

         A12: Mid (b,e1,a) and

         A13: (p,a) // (c,e1) by A5, Th19;

        

         A14: not (p,c,a) are_collinear

        proof

          

           A15: (p,c,p) are_collinear by DIRAF: 31;

          assume (p,c,a) are_collinear ;

          hence contradiction by A1, A4, A11, A15, DIRAF: 32;

        end;

        

         A16: a <> e1

        proof

          assume a = e1;

          then (a,p) // (a,c) by A13, DIRAF: 2;

          then Mid (a,p,c) or Mid (a,c,p) by DIRAF: 7;

          then (a,p,c) are_collinear or (a,c,p) are_collinear by DIRAF: 28;

          hence contradiction by A14, DIRAF: 30;

        end;

        consider e4 such that

         A17: (e1,c) // (c,e4) and

         A18: (e1,b) // (p,e4) by A6, A9, ANALOAF:def 5;

        consider e2 such that

         A19: (a,c) // (c,e2) and

         A20: (a,b) // (p,e2) by A6, A9, ANALOAF:def 5;

        consider e3 such that

         A21: (p,c) // (c,e3) and

         A22: (p,a) // (e2,e3) by A10, A19, ANALOAF:def 5;

        

         A23: not (a,b,c) are_collinear

        proof

          assume (a,b,c) are_collinear ;

          then

           A24: (b,c,a) are_collinear by DIRAF: 30;

          

           A25: (b,c,b) are_collinear by DIRAF: 31;

          (b,c,p) are_collinear by A4, DIRAF: 30;

          hence contradiction by A1, A9, A24, A25, DIRAF: 32;

        end;

        

         A26: c <> e2

        proof

          assume

           A27: c = e2;

          (p,c) // (c,b) by A6, DIRAF: 2;

          then (a,b) // (c,b) by A11, A20, A27, DIRAF: 3;

          then (b,a) // (b,c) by DIRAF: 2;

          then Mid (b,a,c) or Mid (b,c,a) by DIRAF: 7;

          then (b,a,c) are_collinear or (b,c,a) are_collinear by DIRAF: 28;

          hence contradiction by A23, DIRAF: 30;

        end;

        

         A28: e2 <> e3

        proof

          assume e2 = e3;

          then (c,e2) // (p,c) by A21, DIRAF: 2;

          then (a,c) // (p,c) by A19, A26, DIRAF: 3;

          then (c,a) // (c,p) by DIRAF: 2;

          then Mid (c,a,p) or Mid (c,p,a) by DIRAF: 7;

          then (c,a,p) are_collinear or (c,p,a) are_collinear by DIRAF: 28;

          hence contradiction by A14, DIRAF: 30;

        end;

        

         A29: c <> e1

        proof

          assume c = e1;

          then (b,c,a) are_collinear by A12, DIRAF: 28;

          hence contradiction by A23, DIRAF: 30;

        end;

        

         A30: p <> e4

        proof

          assume p = e4;

          then (c,e1) // (p,c) by A17, DIRAF: 2;

          then (p,a) // (p,c) by A13, A29, DIRAF: 3;

          then Mid (p,a,c) or Mid (p,c,a) by DIRAF: 7;

          then (p,a,c) are_collinear or (p,c,a) are_collinear by DIRAF: 28;

          hence contradiction by A14, DIRAF: 30;

        end;

         Mid (e1,c,e4) by A17, DIRAF:def 3;

        then Mid (e4,c,e1) by DIRAF: 9;

        then

         A31: (e4,c) // (c,e1) by DIRAF:def 3;

        (c,e1) // (e2,e3) by A3, A13, A22, ANALOAF:def 5;

        then

         A32: (e4,c) // (e2,e3) by A29, A31, DIRAF: 3;

        

         A33: e2 <> e4

        proof

          assume e2 = e4;

          then (c,e2) // (e1,c) by A17, DIRAF: 2;

          then (a,c) // (e1,c) by A19, A26, DIRAF: 3;

          then (c,e1) // (c,a) by DIRAF: 2;

          then (p,a) // (c,a) by A13, A29, DIRAF: 3;

          then (a,p) // (a,c) by DIRAF: 2;

          then Mid (a,p,c) or Mid (a,c,p) by DIRAF: 7;

          then (a,p,c) are_collinear or (a,c,p) are_collinear by DIRAF: 28;

          hence contradiction by A14, DIRAF: 30;

        end;

        

         A34: c <> e3

        proof

          assume c = e3;

          then (c,e2) // (a,p) by A22, DIRAF: 2;

          then (a,c) // (a,p) by A19, A26, DIRAF: 3;

          then Mid (a,c,p) or Mid (a,p,c) by DIRAF: 7;

          then (a,c,p) are_collinear or (a,p,c) are_collinear by DIRAF: 28;

          hence contradiction by A14, DIRAF: 30;

        end;

        

         A35: p <> e3 by A11, A21, ANALOAF:def 5;

        

         A36: not (p,e3,e2) are_collinear

        proof

          (p,c) // (c,b) by A2, DIRAF:def 3;

          then

           A37: (p,c) // (p,b) by ANALOAF:def 5;

          (p,c) // (p,e3) by A21, ANALOAF:def 5;

          then (p,b) // (p,e3) by A11, A37, ANALOAF:def 5;

          then Mid (p,b,e3) or Mid (p,e3,b) by DIRAF: 7;

          then (p,b,e3) are_collinear or (p,e3,b) are_collinear by DIRAF: 28;

          then

           A38: (p,e3,b) are_collinear by DIRAF: 30;

          

           A39: (p,e3,p) are_collinear by DIRAF: 31;

          (a,c) // (a,e2) by A19, ANALOAF:def 5;

          then Mid (a,c,e2) or Mid (a,e2,c) by DIRAF: 7;

          then (a,c,e2) are_collinear or (a,e2,c) are_collinear by DIRAF: 28;

          then

           A40: (c,e2,a) are_collinear by DIRAF: 30;

          (p,c) // (p,e3) by A21, ANALOAF:def 5;

          then Mid (p,c,e3) or Mid (p,e3,c) by DIRAF: 7;

          then (p,c,e3) are_collinear or (p,e3,c) are_collinear by DIRAF: 28;

          then

           A41: (p,e3,c) are_collinear by DIRAF: 30;

          assume (p,e3,e2) are_collinear ;

          then (p,e3,a) are_collinear by A26, A41, A40, DIRAF: 35;

          hence contradiction by A1, A35, A38, A39, DIRAF: 32;

        end;

        then

         A42: not (e3,e2,p) are_collinear by DIRAF: 30;

        consider e5 such that

         A43: (e4,e2) // (c,e5) and

         A44: (e4,c) // (e2,e5) and

         A45: e2 <> e5 by ANALOAF:def 5;

        

         A46: b <> e1

        proof

          (p,c) // (c,b) by A2, DIRAF:def 3;

          then

           A47: (c,b) // (p,c) by DIRAF: 2;

          assume b = e1;

          then (p,a) // (p,c) by A9, A13, A47, DIRAF: 3;

          then Mid (p,a,c) or Mid (p,c,a) by DIRAF: 7;

          then (p,a,c) are_collinear or (p,c,a) are_collinear by DIRAF: 28;

          hence contradiction by A14, DIRAF: 30;

        end;

        

         A48: c <> e4

        proof

          assume

           A49: c = e4;

          (p,c) // (c,b) by A2, DIRAF:def 3;

          then (e1,b) // (c,b) by A11, A18, A49, DIRAF: 3;

          then (b,e1) // (b,c) by DIRAF: 2;

          then Mid (b,e1,c) or Mid (b,c,e1) by DIRAF: 7;

          then (b,e1,c) are_collinear or (b,c,e1) are_collinear by DIRAF: 28;

          then

           A50: (b,e1,c) are_collinear by DIRAF: 30;

          

           A51: (b,e1,b) are_collinear by DIRAF: 31;

          (b,e1,a) are_collinear by A12, DIRAF: 28;

          hence contradiction by A23, A46, A50, A51, DIRAF: 32;

        end;

        

         A52: c <> e5

        proof

          assume c = e5;

          then (c,e4) // (c,e2) by A44, DIRAF: 2;

          then (e1,c) // (c,e2) by A17, A48, DIRAF: 3;

          then (c,e2) // (e1,c) by DIRAF: 2;

          then (a,c) // (e1,c) by A19, A26, DIRAF: 3;

          then (c,e1) // (c,a) by DIRAF: 2;

          then (p,a) // (c,a) by A13, A29, DIRAF: 3;

          then (a,p) // (a,c) by DIRAF: 2;

          then Mid (a,p,c) or Mid (a,c,p) by DIRAF: 7;

          then (a,p,c) are_collinear or (a,c,p) are_collinear by DIRAF: 28;

          hence contradiction by A14, DIRAF: 30;

        end;

         Mid (a,e1,b) by A12, DIRAF: 9;

        then

         A53: (a,e1) // (e1,b) by DIRAF:def 3;

        then (a,e1) // (a,b) by ANALOAF:def 5;

        then (a,b) // (e1,b) by A16, A53, ANALOAF:def 5;

        then (e1,b) // (p,e2) by A7, A20, ANALOAF:def 5;

        then

         A54: (p,e4) // (p,e2) by A18, A46, ANALOAF:def 5;

         Mid (p,c,e3) by A21, DIRAF:def 3;

        then Mid (p,e4,e2) by A36, A32, A30, A54, Th16;

        then

         A55: (p,e4) // (e4,e2) by DIRAF:def 3;

        then (p,e4) // (p,e2) by ANALOAF:def 5;

        then

         A56: (p,e2) // (e4,e2) by A30, A55, ANALOAF:def 5;

        then

         A57: (p,e2) // (c,e5) by A43, A33, DIRAF: 3;

        p <> e2

        proof

          assume p = e2;

          then Mid (a,c,p) by A19, DIRAF:def 3;

          hence contradiction by A14, DIRAF: 9, DIRAF: 28;

        end;

        then

         A58: (a,b) // (e4,e2) by A20, A56, DIRAF: 3;

        then

         A59: (a,b) // (c,e5) by A43, A33, DIRAF: 3;

        

         A60: e5 <> e3

        proof

          assume e5 = e3;

          then (c,e3) // (a,b) by A59, DIRAF: 2;

          then (p,c) // (a,b) by A21, A34, DIRAF: 3;

          then (c,p) // (b,a) by DIRAF: 2;

          then (b,c) // (b,a) by A6, A11, DIRAF: 3;

          then Mid (b,c,a) or Mid (b,a,c) by DIRAF: 7;

          then (b,c,a) are_collinear or (b,a,c) are_collinear by DIRAF: 28;

          hence contradiction by A23, DIRAF: 30;

        end;

        (c,e1) // (e4,c) by A17, DIRAF: 2;

        then (c,e1) // (e2,e5) by A44, A48, DIRAF: 3;

        then (p,a) // (e2,e5) by A13, A29, DIRAF: 3;

        then (e2,e3) // (e2,e5) by A3, A22, ANALOAF:def 5;

        then Mid (e2,e3,e5) or Mid (e2,e5,e3) by DIRAF: 7;

        then (e2,e3,e5) are_collinear or (e2,e5,e3) are_collinear by DIRAF: 28;

        then

         A61: (e2,e3,e5) are_collinear by DIRAF: 30;

         Mid (p,c,e3) by A21, DIRAF:def 3;

        then

         A62: Mid (e3,c,p) by DIRAF: 9;

        (e3,c) // (c,p) by A21, DIRAF: 2;

        then

        consider x such that

         A63: (e5,c) // (c,x) and

         A64: (e5,e3) // (p,x) by A34, ANALOAF:def 5;

        

         A65: (c,e5) // (x,c) by A63, DIRAF: 2;

         Mid (p,c,e3) by A21, DIRAF:def 3;

        then Mid (e3,c,p) by DIRAF: 9;

        then (e3,c) // (c,p) by DIRAF:def 3;

        then (e3,c) // (e3,p) by ANALOAF:def 5;

        then (e3,p) // (e3,c) by DIRAF: 2;

        then not Mid (e2,e3,e5) by A60, A57, A42, Th17;

        then Mid (e3,e2,e5) or Mid (e2,e5,e3) by A61, DIRAF: 29;

        then (e3,e2) // (e2,e5) or Mid (e3,e5,e2) by DIRAF: 9, DIRAF:def 3;

        then (e3,e2) // (e3,e5) or (e3,e5) // (e5,e2) by ANALOAF:def 5, DIRAF:def 3;

        then

         A66: (e3,e5) // (e3,e2) by ANALOAF:def 5, DIRAF: 2;

        (c,e5) // (p,e2) by A57, DIRAF: 2;

        then Mid (e3,e5,e2) by A34, A42, A66, A62, Th15;

        then Mid (e2,e5,e3) by DIRAF: 9;

        then

         A67: (e2,e5) // (e5,e3) by DIRAF:def 3;

        then (e2,e5) // (e2,e3) by ANALOAF:def 5;

        then (e2,e3) // (e5,e3) by A45, A67, ANALOAF:def 5;

        then (p,a) // (e5,e3) by A22, A28, DIRAF: 3;

        then (p,a) // (p,x) by A64, A60, DIRAF: 3;

        then

         A68: (p,x) // (p,a) by DIRAF: 2;

        (a,b) // (c,e5) by A43, A33, A58, DIRAF: 3;

        then

         A69: (a,b) // (x,c) by A52, A65, DIRAF: 3;

        then (c,x) // (b,a) by DIRAF: 2;

        hence thesis by A1, A2, A11, A69, A68, Th15;

      end;

      

       A70: a = c implies (a,b) // (a,c) & Mid (p,a,a) by DIRAF: 4, DIRAF: 10;

      

       A71: p = c implies (a,b) // (c,c) & Mid (p,c,a) by DIRAF: 4, DIRAF: 10;

      b = c implies (a,b) // (a,c) & Mid (p,a,a) by DIRAF: 1, DIRAF: 10;

      hence thesis by A8, A70, A71;

    end;

    theorem :: PASCH:22

    ex x st (a,x) // (b,c) & (a,b) // (x,c)

    proof

       A1:

      now

        consider e3 such that

         A2: Mid (b,c,e3) and

         A3: c <> e3 by DIRAF: 13;

        

         A4: (b,c) // (c,e3) by A2, DIRAF:def 3;

        assume

         A5: not (a,b,c) are_collinear ;

        then

         A6: b <> c by DIRAF: 31;

        then

        consider e4 such that

         A7: (a,c) // (c,e4) and

         A8: (a,b) // (e3,e4) by A4, ANALOAF:def 5;

        

         A9: Mid (a,c,e4) by A7, DIRAF:def 3;

        then Mid (e4,c,a) by DIRAF: 9;

        then

         A10: (e4,c) // (c,a) by DIRAF:def 3;

        

         A11: e4 <> c

        proof

          assume

           A12: e4 = c;

          (e3,c) // (c,b) by A4, DIRAF: 2;

          then (a,b) // (c,b) by A3, A8, A12, DIRAF: 3;

          then (b,a) // (b,c) by DIRAF: 2;

          then Mid (b,a,c) or Mid (b,c,a) by DIRAF: 7;

          then (b,a,c) are_collinear or (b,c,a) are_collinear by DIRAF: 28;

          hence contradiction by A5, DIRAF: 30;

        end;

        

         A13: not (e4,c,e3) are_collinear

        proof

          (b,c,e3) are_collinear by A2, DIRAF: 28;

          then

           A14: (c,e3,b) are_collinear by DIRAF: 30;

          assume

           A15: (e4,c,e3) are_collinear ;

          

           A16: (c,e3,c) are_collinear by DIRAF: 31;

          

           A17: (e4,c,c) are_collinear by DIRAF: 31;

          (e4,c,a) are_collinear by A9, DIRAF: 9, DIRAF: 28;

          then (c,e3,a) are_collinear by A11, A15, A17, DIRAF: 32;

          hence contradiction by A5, A3, A14, A16, DIRAF: 32;

        end;

        (b,c) // (c,e3) by A2, DIRAF:def 3;

        then

         A18: (c,e3) // (b,c) by DIRAF: 2;

        consider e1 such that

         A19: Mid (c,a,e1) and

         A20: a <> e1 by DIRAF: 13;

        

         A21: (c,a) // (a,e1) by A19, DIRAF:def 3;

        

         A22: a <> c by A5, DIRAF: 31;

        then

        consider e2 such that

         A23: (b,a) // (a,e2) and

         A24: (b,c) // (e1,e2) by A21, ANALOAF:def 5;

        (c,a) // (c,e1) by A21, ANALOAF:def 5;

        then (e4,c) // (c,e1) by A22, A10, DIRAF: 3;

        then

         A25: Mid (e4,c,e1) by DIRAF:def 3;

        then

        consider e5 such that

         A26: Mid (e4,e3,e5) and

         A27: (c,e3) // (e1,e5) by A11, Th20;

        

         A28: e4 <> e3

        proof

          assume e4 = e3;

          then Mid (a,c,e3) by A7, DIRAF:def 3;

          then

           A29: (e3,c,a) are_collinear by DIRAF: 9, DIRAF: 28;

          

           A30: (e3,c,c) are_collinear by DIRAF: 31;

          (e3,c,b) are_collinear by A2, DIRAF: 9, DIRAF: 28;

          hence contradiction by A5, A3, A29, A30, DIRAF: 32;

        end;

        then

         A31: e4 <> e5 by A26, DIRAF: 8;

        

         A32: e1 <> e4 by A25, A11, DIRAF: 8;

        

         A33: not (e1,e4,e3) are_collinear

        proof

          (e4,c,e1) are_collinear by A25, DIRAF: 28;

          then

           A34: (e4,e1,c) are_collinear by DIRAF: 30;

          assume (e1,e4,e3) are_collinear ;

          then

           A35: (e4,e1,e3) are_collinear by DIRAF: 30;

          (e4,e1,e4) are_collinear by DIRAF: 31;

          hence contradiction by A32, A13, A35, A34, DIRAF: 32;

        end;

        

         A36: not (e1,e5,e4) are_collinear

        proof

          (e4,e3,e5) are_collinear by A26, DIRAF: 28;

          then

           A37: (e5,e4,e3) are_collinear by DIRAF: 30;

          assume (e1,e5,e4) are_collinear ;

          then

           A38: (e5,e4,e1) are_collinear by DIRAF: 30;

          (e5,e4,e4) are_collinear by DIRAF: 31;

          hence contradiction by A31, A33, A38, A37, DIRAF: 32;

        end;

        then

         A39: e1 <> e5 by DIRAF: 31;

         Mid (e1,c,e4) by A25, DIRAF: 9;

        then

        consider e6 such that

         A40: Mid (e1,e6,e5) and

         A41: (e5,e4) // (e6,c) by A36, Th21;

        

         A42: c <> e1 by A19, A20, DIRAF: 8;

        

         A43: not (c,e1,b) are_collinear

        proof

          (c,a,e1) are_collinear by A19, DIRAF: 28;

          then

           A44: (c,e1,a) are_collinear by DIRAF: 30;

          

           A45: (c,e1,c) are_collinear by DIRAF: 31;

          assume (c,e1,b) are_collinear ;

          hence contradiction by A5, A42, A44, A45, DIRAF: 32;

        end;

        

         A46: e5 <> e3

        proof

          assume e5 = e3;

          then (e3,c) // (e3,e1) by A27, DIRAF: 2;

          then Mid (e3,c,e1) or Mid (e3,e1,c) by DIRAF: 7;

          then (e3,c,e1) are_collinear or (e3,e1,c) are_collinear by DIRAF: 28;

          then

           A47: (e3,c,e1) are_collinear by DIRAF: 30;

          

           A48: (e3,c,c) are_collinear by DIRAF: 31;

          (e3,c,b) are_collinear by A2, DIRAF: 9, DIRAF: 28;

          hence contradiction by A3, A43, A47, A48, DIRAF: 32;

        end;

        

         A49: e1 <> e6

        proof

           Mid (e5,e3,e4) by A26, DIRAF: 9;

          then

           A50: (e5,e3) // (e3,e4) by DIRAF:def 3;

          then (e5,e3) // (e5,e4) by ANALOAF:def 5;

          then

           A51: (e5,e4) // (e3,e4) by A46, A50, ANALOAF:def 5;

          assume e1 = e6;

          then (e3,e4) // (e1,c) by A31, A41, A51, ANALOAF:def 5;

          then

           A52: (a,b) // (e1,c) by A8, A28, DIRAF: 3;

           Mid (e1,a,c) by A19, DIRAF: 9;

          then

           A53: (e1,a) // (a,c) by DIRAF:def 3;

          then (e1,a) // (e1,c) by ANALOAF:def 5;

          then (e1,c) // (a,c) by A20, A53, ANALOAF:def 5;

          then (a,b) // (a,c) by A42, A52, DIRAF: 3;

          then (a,b) // (b,c) or (a,c) // (c,b) by DIRAF: 6;

          then Mid (a,b,c) or Mid (a,c,b) by DIRAF:def 3;

          then (a,b,c) are_collinear or (a,c,b) are_collinear by DIRAF: 28;

          hence contradiction by A5, DIRAF: 30;

        end;

        consider x such that

         A54: Mid (c,x,e6) and

         A55: (e1,e6) // (a,x) by A19, Th19;

        (e1,e6) // (e6,e5) by A40, DIRAF:def 3;

        then (e1,e6) // (e1,e5) by ANALOAF:def 5;

        then (e1,e5) // (a,x) by A55, A49, ANALOAF:def 5;

        then (c,e3) // (a,x) by A27, A39, DIRAF: 3;

        then

         A56: (a,x) // (b,c) by A3, A18, ANALOAF:def 5;

        

         A57: e6 <> c

        proof

          assume e6 = c;

          then x = c by A54, DIRAF: 8;

          then (c,a) // (c,b) by A56, DIRAF: 2;

          then Mid (c,a,b) or Mid (c,b,a) by DIRAF: 7;

          then (c,a,b) are_collinear or (c,b,a) are_collinear by DIRAF: 28;

          hence contradiction by A5, DIRAF: 30;

        end;

        

         A58: a <> e2

        proof

          assume

           A59: a = e2;

          (e1,a) // (a,c) by A21, DIRAF: 2;

          then (b,c) // (a,c) by A20, A24, A59, DIRAF: 3;

          then (c,b) // (c,a) by DIRAF: 2;

          then Mid (c,b,a) or Mid (c,a,b) by DIRAF: 7;

          then (c,b,a) are_collinear or (c,a,b) are_collinear by DIRAF: 28;

          hence contradiction by A5, DIRAF: 30;

        end;

        

         A60: e6 <> x

        proof

          assume e6 = x;

          then (e6,e1) // (e6,a) by A55, DIRAF: 2;

          then Mid (e6,e1,a) or Mid (e6,a,e1) by DIRAF: 7;

          then (e6,e1,a) are_collinear or (e6,a,e1) are_collinear by DIRAF: 28;

          then

           A61: (e6,e1,a) are_collinear by DIRAF: 30;

          (e1,e6,e5) are_collinear by A40, DIRAF: 28;

          then

           A62: (e6,e1,e5) are_collinear by DIRAF: 30;

          (b,c) // (e1,e5) by A3, A4, A27, DIRAF: 3;

          then (e1,e2) // (e1,e5) by A6, A24, ANALOAF:def 5;

          then Mid (e1,e2,e5) or Mid (e1,e5,e2) by DIRAF: 7;

          then (e1,e2,e5) are_collinear or (e1,e5,e2) are_collinear by DIRAF: 28;

          then

           A63: (e1,e5,e2) are_collinear by DIRAF: 30;

          

           A64: (e1,e5,e1) are_collinear by DIRAF: 31;

           Mid (b,a,e2) by A23, DIRAF:def 3;

          then (b,a,e2) are_collinear by DIRAF: 28;

          then

           A65: (a,e2,b) are_collinear by DIRAF: 30;

          (c,a,e1) are_collinear by A19, DIRAF: 28;

          then

           A66: (a,e1,c) are_collinear by DIRAF: 30;

          (e6,e1,e1) are_collinear by DIRAF: 31;

          then (e1,e5,a) are_collinear by A49, A61, A62, DIRAF: 32;

          then

           A67: (a,e1,e2) are_collinear by A39, A63, A64, DIRAF: 32;

          

           A68: (a,e2,a) are_collinear by DIRAF: 31;

          (a,e1,a) are_collinear by DIRAF: 31;

          then (a,e2,c) are_collinear by A20, A67, A66, DIRAF: 32;

          hence contradiction by A5, A58, A65, A68, DIRAF: 32;

        end;

         Mid (e6,x,c) by A54, DIRAF: 9;

        then

         A69: (e6,x) // (x,c) by DIRAF:def 3;

        then (e6,x) // (e6,c) by ANALOAF:def 5;

        then

         A70: (e6,c) // (x,c) by A60, A69, ANALOAF:def 5;

         Mid (e5,e3,e4) by A26, DIRAF: 9;

        then

         A71: (e5,e3) // (e3,e4) by DIRAF:def 3;

        then (e5,e3) // (e5,e4) by ANALOAF:def 5;

        then (e3,e4) // (e5,e4) by A46, A71, ANALOAF:def 5;

        then (a,b) // (e5,e4) by A8, A28, DIRAF: 3;

        then (a,b) // (e6,c) by A31, A41, DIRAF: 3;

        then (a,b) // (x,c) by A57, A70, DIRAF: 3;

        hence thesis by A56;

      end;

      now

         A72:

        now

          assume Mid (a,c,b);

          then (a,c) // (c,b) by DIRAF:def 3;

          then (a,c) // (a,b) by ANALOAF:def 5;

          hence (a,a) // (b,c) & (a,b) // (a,c) by DIRAF: 2, DIRAF: 4;

        end;

         A73:

        now

          assume Mid (b,a,c);

          then Mid (c,a,b) by DIRAF: 9;

          then (c,a) // (a,b) by DIRAF:def 3;

          then (c,a) // (c,b) by ANALOAF:def 5;

          hence (a,c) // (b,c) & (a,b) // (c,c) by DIRAF: 2, DIRAF: 4;

        end;

        

         A74: Mid (a,b,c) implies (a,b) // (b,c) & (a,b) // (b,c) by DIRAF:def 3;

        assume (a,b,c) are_collinear ;

        hence thesis by A74, A73, A72, DIRAF: 29;

      end;

      hence thesis by A1;

    end;

    theorem :: PASCH:23

    

     Th23: (a,b) // (c,d) & not (a,b,c) are_collinear implies ex x st Mid (a,x,d) & Mid (b,x,c)

    proof

      assume that

       A1: (a,b) // (c,d) and

       A2: not (a,b,c) are_collinear ;

       A3:

      now

        consider e1 such that

         A4: (a,b) // (d,e1) and

         A5: (a,d) // (b,e1) and

         A6: b <> e1 by ANALOAF:def 5;

        

         A7: a <> b by A2, DIRAF: 31;

        then (c,d) // (d,e1) by A1, A4, ANALOAF:def 5;

        then

         A8: Mid (c,d,e1) by DIRAF:def 3;

        

         A9: a <> d

        proof

          assume a = d;

          then (b,a) // (a,c) by A1, DIRAF: 2;

          then Mid (b,a,c) by DIRAF:def 3;

          then (b,a,c) are_collinear by DIRAF: 28;

          hence contradiction by A2, DIRAF: 30;

        end;

        

         A10: not (a,b,d) are_collinear

        proof

           A11:

          now

            assume (a,b) // (a,d);

            then (c,d) // (a,d) by A1, A7, ANALOAF:def 5;

            then (d,c) // (d,a) by DIRAF: 2;

            then (d,c) '||' (d,a) by DIRAF:def 4;

            hence (d,c,a) are_collinear by DIRAF:def 5;

          end;

          

           A12: (d,a,a) are_collinear by DIRAF: 31;

           A13:

          now

            assume (a,b) // (d,a);

            then (c,d) // (d,a) by A1, A7, ANALOAF:def 5;

            then Mid (c,d,a) by DIRAF:def 3;

            then (c,d,a) are_collinear by DIRAF: 28;

            hence (d,c,a) are_collinear by DIRAF: 30;

          end;

          assume

           A14: (a,b,d) are_collinear ;

          then

           A15: (d,a,b) are_collinear by DIRAF: 30;

          (a,b) '||' (a,d) by A14, DIRAF:def 5;

          then (d,a,c) are_collinear by A11, A13, DIRAF: 30, DIRAF:def 4;

          hence contradiction by A2, A9, A12, A15, DIRAF: 32;

        end;

        consider e2 such that

         A16: (c,d) // (b,e2) and

         A17: (c,b) // (d,e2) and

         A18: d <> e2 by ANALOAF:def 5;

        assume

         A19: c <> d;

        then (a,b) // (b,e2) by A1, A16, DIRAF: 3;

        then

         A20: Mid (a,b,e2) by DIRAF:def 3;

        

         A21: not (c,d,b) are_collinear

        proof

           A22:

          now

            assume (c,d) // (c,b);

            then (a,b) // (c,b) by A1, A19, DIRAF: 3;

            then (b,a) // (b,c) by DIRAF: 2;

            then Mid (b,a,c) or Mid (b,c,a) by DIRAF: 7;

            then (b,a,c) are_collinear or (b,c,a) are_collinear by DIRAF: 28;

            hence contradiction by A2, DIRAF: 30;

          end;

          assume (c,d,b) are_collinear ;

          then (c,d) '||' (c,b) by DIRAF:def 5;

          then (c,d) // (c,b) or (c,d) // (b,c) by DIRAF:def 4;

          then (a,b) // (b,c) by A1, A19, A22, DIRAF: 3;

          then Mid (a,b,c) by DIRAF:def 3;

          hence contradiction by A2, DIRAF: 28;

        end;

        

         A23: (b,c,c) are_collinear by DIRAF: 31;

        

         A24: (d,a,a) are_collinear by DIRAF: 31;

        

         A25: c <> e1

        proof

          assume c = e1;

          then (c,d) // (d,c) by A1, A4, A7, ANALOAF:def 5;

          hence contradiction by A19, ANALOAF:def 5;

        end;

         not (c,b,e1) are_collinear

        proof

          (c,d,e1) are_collinear by A8, DIRAF: 28;

          then

           A26: (c,e1,d) are_collinear by DIRAF: 30;

          assume (c,b,e1) are_collinear ;

          then

           A27: (c,e1,b) are_collinear by DIRAF: 30;

          (c,e1,c) are_collinear by DIRAF: 31;

          hence contradiction by A25, A21, A27, A26, DIRAF: 32;

        end;

        then

        consider x such that

         A28: Mid (c,x,b) and

         A29: (b,e1) // (x,d) by A8, Th21;

        

         A30: Mid (b,x,c) by A28, DIRAF: 9;

        (a,d) // (x,d) by A5, A6, A29, DIRAF: 3;

        then (d,a) // (d,x) by DIRAF: 2;

        then Mid (d,a,x) or Mid (d,x,a) by DIRAF: 7;

        then (d,a,x) are_collinear or (d,x,a) are_collinear by DIRAF: 28;

        then

         A31: (d,a,x) are_collinear by DIRAF: 30;

        

         A32: b <> c by A2, DIRAF: 31;

        

         A33: a <> e2

        proof

          assume a = e2;

          then (a,b) // (b,a) by A1, A19, A16, DIRAF: 3;

          hence contradiction by A7, ANALOAF:def 5;

        end;

         not (a,d,e2) are_collinear

        proof

          (a,b,e2) are_collinear by A20, DIRAF: 28;

          then

           A34: (a,e2,b) are_collinear by DIRAF: 30;

          assume (a,d,e2) are_collinear ;

          then

           A35: (a,e2,d) are_collinear by DIRAF: 30;

          (a,e2,a) are_collinear by DIRAF: 31;

          hence contradiction by A33, A10, A35, A34, DIRAF: 32;

        end;

        then

        consider y such that

         A36: Mid (a,y,d) and

         A37: (d,e2) // (y,b) by A20, Th21;

        

         A38: (b,c,b) are_collinear by DIRAF: 31;

        (c,b) // (y,b) by A17, A18, A37, DIRAF: 3;

        then (b,c) // (b,y) by DIRAF: 2;

        then Mid (b,c,y) or Mid (b,y,c) by DIRAF: 7;

        then (b,c,y) are_collinear or (b,y,c) are_collinear by DIRAF: 28;

        then

         A39: (b,c,y) are_collinear by DIRAF: 30;

        

         A40: (c,x,b) are_collinear by A28, DIRAF: 28;

        then (b,c,x) are_collinear by DIRAF: 30;

        then

         A41: (x,y,c) are_collinear by A32, A39, A23, DIRAF: 32;

        (a,y,d) are_collinear by A36, DIRAF: 28;

        then (d,a,y) are_collinear by DIRAF: 30;

        then

         A42: (x,y,a) are_collinear by A9, A31, A24, DIRAF: 32;

        (b,c,x) are_collinear by A40, DIRAF: 30;

        then (x,y,b) are_collinear by A32, A39, A38, DIRAF: 32;

        then Mid (a,x,d) by A2, A36, A42, A41, DIRAF: 32;

        hence thesis by A30;

      end;

      now

        assume

         A43: c = d;

        take x = c;

        thus Mid (a,x,d) & Mid (b,x,c) by A43, DIRAF: 10;

      end;

      hence thesis by A3;

    end;

    theorem :: PASCH:24

    OAS is Fanoian by Th23;

    theorem :: PASCH:25

    (a,b) '||' (c,d) & (a,c) '||' (b,d) & not (a,b,c) are_collinear implies ex x st (x,a,d) are_collinear & (x,b,c) are_collinear

    proof

      assume that

       A1: (a,b) '||' (c,d) and

       A2: (a,c) '||' (b,d) and

       A3: not (a,b,c) are_collinear ;

      (a,b) // (c,d) by A1, A2, A3, Th14;

      then

      consider x such that

       A4: Mid (a,x,d) and

       A5: Mid (b,x,c) by A3, Th23;

      (b,x,c) are_collinear by A5, DIRAF: 28;

      then

       A6: (x,b,c) are_collinear by DIRAF: 30;

      (a,x,d) are_collinear by A4, DIRAF: 28;

      then (x,a,d) are_collinear by DIRAF: 30;

      hence thesis by A6;

    end;

    theorem :: PASCH:26

    (a,b) '||' (c,d) & not (a,b,c) are_collinear & (p,a,d) are_collinear & (p,b,c) are_collinear implies not (p,a,b) are_collinear

    proof

      assume that

       A1: (a,b) '||' (c,d) and

       A2: not (a,b,c) are_collinear and

       A3: (p,a,d) are_collinear and

       A4: (p,b,c) are_collinear ;

      

       A5: (p,a,a) are_collinear by DIRAF: 31;

      assume (p,a,b) are_collinear ;

      then

       A6: (a,b,d) are_collinear by A2, A3, A4, A5, DIRAF: 32;

      

       A7: (a,b) '||' (d,c) by A1, DIRAF: 22;

      a <> b by A2, DIRAF: 31;

      hence contradiction by A2, A6, A7, DIRAF: 33;

    end;

    theorem :: PASCH:27

    

     Th27: Mid (a,b,d) & Mid (b,x,c) & not (a,b,c) are_collinear implies ex y st Mid (a,y,c) & Mid (y,x,d)

    proof

      assume that

       A1: Mid (a,b,d) and

       A2: Mid (b,x,c) and

       A3: not (a,b,c) are_collinear ;

       A4:

      now

        assume

         A5: b = d;

        take y = c;

        thus Mid (a,y,c) & Mid (d,x,y) by A2, A5, DIRAF: 10;

        thus Mid (a,y,c) & Mid (y,x,d) by A2, A5, DIRAF: 9, DIRAF: 10;

      end;

      

       A6: Mid (d,b,a) by A1, DIRAF: 9;

       A7:

      now

        assume that

         A8: b <> d and

         A9: x <> b;

        (d,b) // (b,a) by A6, DIRAF:def 3;

        then

        consider e1 such that

         A10: (x,b) // (b,e1) and

         A11: (x,d) // (a,e1) by A8, ANALOAF:def 5;

        

         A12: Mid (x,b,e1) by A10, DIRAF:def 3;

        then

         A13: Mid (e1,b,x) by DIRAF: 9;

        then

         A14: Mid (e1,x,c) by A2, A9, DIRAF: 12;

        

         A15: c <> e1

        proof

          assume c = e1;

          then Mid (x,b,x) by A2, A9, A13, DIRAF: 8, DIRAF: 12;

          hence contradiction by A9, DIRAF: 8;

        end;

        

         A16: x <> e1 by A9, A12, DIRAF: 8;

        

         A17: not (c,a,e1) are_collinear

        proof

          (x,b,e1) are_collinear by A12, DIRAF: 28;

          then

           A18: (x,e1,b) are_collinear by DIRAF: 30;

          assume (c,a,e1) are_collinear ;

          then

           A19: (c,e1,a) are_collinear by DIRAF: 30;

          (c,x,e1) are_collinear by A14, DIRAF: 9, DIRAF: 28;

          then

           A20: (c,e1,x) are_collinear by DIRAF: 30;

          

           A21: (c,e1,c) are_collinear by DIRAF: 31;

          (c,e1,e1) are_collinear by DIRAF: 31;

          then (c,e1,b) are_collinear by A16, A20, A18, DIRAF: 35;

          hence contradiction by A3, A15, A19, A21, DIRAF: 32;

        end;

         Mid (c,x,e1) by A14, DIRAF: 9;

        then

        consider y such that

         A22: Mid (c,y,a) and

         A23: (a,e1) // (y,x) by A17, Th21;

        a <> e1 by A17, DIRAF: 31;

        then (x,d) // (y,x) by A11, A23, DIRAF: 3;

        then (d,x) // (x,y) by DIRAF: 2;

        then Mid (d,x,y) by DIRAF:def 3;

        then

         A24: Mid (y,x,d) by DIRAF: 9;

         Mid (a,y,c) by A22, DIRAF: 9;

        hence thesis by A24;

      end;

      now

        assume that b <> d and

         A25: x = b;

        take y = a;

        thus Mid (a,y,c) & Mid (y,x,d) by A1, A25, DIRAF: 10;

      end;

      hence thesis by A7, A4;

    end;

    theorem :: PASCH:28

    OAS is satisfying_Ext_Bet_Pasch by Th27;

    theorem :: PASCH:29

    

     Th29: Mid (a,b,d) & Mid (a,x,c) & not (a,b,c) are_collinear implies ex y st Mid (b,y,c) & Mid (x,y,d)

    proof

      assume that

       A1: Mid (a,b,d) and

       A2: Mid (a,x,c) and

       A3: not (a,b,c) are_collinear ;

      

       A4: b <> c by A3, DIRAF: 31;

      

       A5: a <> b by A3, DIRAF: 31;

       A6:

      now

        assume that

         A7: b <> d and

         A8: x <> c and

         A9: a <> x;

        

         A10: a <> d by A1, A7, DIRAF: 8;

        consider e1 such that

         A11: Mid (a,d,e1) and

         A12: (x,d) // (c,e1) by A2, A9, Th20;

        

         A13: Mid (e1,d,a) by A11, DIRAF: 9;

        

         A14: (d,b,a) are_collinear by A1, DIRAF: 9, DIRAF: 28;

        

         A15: not (a,x,b) are_collinear

        proof

          

           A16: (a,x,a) are_collinear by DIRAF: 31;

          assume

           A17: (a,x,b) are_collinear ;

          (a,x,c) are_collinear by A2, DIRAF: 28;

          hence contradiction by A3, A9, A17, A16, DIRAF: 32;

        end;

        

         A18: not (x,d,a) are_collinear

        proof

          assume (x,d,a) are_collinear ;

          then

           A19: (d,a,x) are_collinear by DIRAF: 30;

          

           A20: (d,a,a) are_collinear by DIRAF: 31;

          (d,a,b) are_collinear by A14, DIRAF: 30;

          hence contradiction by A10, A15, A19, A20, DIRAF: 32;

        end;

        then

         A21: x <> d by DIRAF: 31;

        

         A22: Mid (d,b,a) by A1, DIRAF: 9;

         Mid (b,d,e1) by A1, A11, DIRAF: 11;

        then Mid (e1,d,b) by DIRAF: 9;

        then Mid (e1,b,a) by A22, A13, DIRAF: 12;

        then

         A23: (e1,b) // (b,a) by DIRAF:def 3;

        e1 <> b by A7, A22, A13, DIRAF: 14;

        then

        consider e2 such that

         A24: (c,b) // (b,e2) and

         A25: (c,e1) // (a,e2) by A23, ANALOAF:def 5;

        

         A26: Mid (c,b,e2) by A24, DIRAF:def 3;

        then

         A27: (c,b,e2) are_collinear by DIRAF: 28;

         Mid (c,x,a) by A2, DIRAF: 9;

        then

        consider y such that

         A28: Mid (c,y,e2) and

         A29: (a,e2) // (x,y) by Th19;

        

         A30: Mid (c,b,y) or Mid (c,y,b) by A26, A28, DIRAF: 17;

        

         A31: c <> e2 by A4, A24, ANALOAF:def 5;

         A32:

        now

          (c,b,e2) are_collinear by A26, DIRAF: 28;

          then

           A33: (c,e2,b) are_collinear by DIRAF: 30;

          (c,y,e2) are_collinear by A28, DIRAF: 28;

          then

           A34: (c,e2,y) are_collinear by DIRAF: 30;

          (c,e2,c) are_collinear by DIRAF: 31;

          then

           A35: (b,y,c) are_collinear by A31, A34, A33, DIRAF: 32;

          (a,x,c) are_collinear by A2, DIRAF: 28;

          then

           A36: (x,a,c) are_collinear by DIRAF: 30;

          

           A37: Mid (c,x,a) by A2, DIRAF: 9;

          assume

           A38: Mid (x,d,y);

          then

          consider c9 such that

           A39: Mid (x,c9,a) and

           A40: Mid (c9,b,y) by A22, A18, Th27;

          (x,c9,a) are_collinear by A39, DIRAF: 28;

          then

           A41: (x,a,c9) are_collinear by DIRAF: 30;

          

           A42: b <> y

          proof

            assume b = y;

            then (x,d,b) are_collinear by A38, DIRAF: 28;

            then

             A43: (d,b,x) are_collinear by DIRAF: 30;

            

             A44: (d,b,b) are_collinear by DIRAF: 31;

            (a,x,c) are_collinear by A2, DIRAF: 28;

            then (d,b,c) are_collinear by A9, A14, A43, DIRAF: 35;

            hence contradiction by A3, A7, A14, A44, DIRAF: 32;

          end;

          (c9,b,y) are_collinear by A40, DIRAF: 28;

          then

           A45: (b,y,c9) are_collinear by DIRAF: 30;

          then

           A46: (c,c9,c) are_collinear by A42, A35, DIRAF: 32;

          (b,y,b) are_collinear by DIRAF: 31;

          then

           A47: (c,c9,b) are_collinear by A42, A35, A45, DIRAF: 32;

          (x,a,a) are_collinear by DIRAF: 31;

          then (c,c9,a) are_collinear by A9, A36, A41, DIRAF: 32;

          then Mid (x,c,a) by A3, A39, A47, A46, DIRAF: 32;

          hence contradiction by A8, A37, DIRAF: 14;

        end;

        

         A48: a <> e2

        proof

          assume a = e2;

          then Mid (c,b,a) by A24, DIRAF:def 3;

          hence contradiction by A3, DIRAF: 9, DIRAF: 28;

        end;

        

         A49: (e1,d,a) are_collinear by A11, DIRAF: 9, DIRAF: 28;

        

         A50: c <> e1

        proof

          assume c = e1;

          then

           A51: (d,a,c) are_collinear by A49, DIRAF: 30;

          

           A52: (d,a,a) are_collinear by DIRAF: 31;

          (d,a,b) are_collinear by A14, DIRAF: 30;

          hence contradiction by A3, A10, A51, A52, DIRAF: 32;

        end;

        then (x,d) // (a,e2) by A12, A25, DIRAF: 3;

        then (x,d) // (x,y) by A48, A29, DIRAF: 3;

        then

         A53: Mid (x,d,y) or Mid (x,y,d) by DIRAF: 7;

        then

         A54: Mid (d,y,x) by A32, DIRAF: 9;

        now

          

           A55: b <> e2

          proof

            

             A56: (a,b) // (b,d) by A1, DIRAF:def 3;

            assume

             A57: b = e2;

            (c,e1) // (x,d) by A12, DIRAF: 2;

            then (a,b) // (x,d) by A25, A50, A57, ANALOAF:def 5;

            then (x,d) // (b,d) by A5, A56, ANALOAF:def 5;

            then (d,x) // (d,b) by DIRAF: 2;

            then Mid (d,x,b) or Mid (d,b,x) by DIRAF: 7;

            then (d,x,b) are_collinear or (d,b,x) are_collinear by DIRAF: 28;

            then

             A58: (d,b,x) are_collinear by DIRAF: 30;

            (d,b,b) are_collinear by DIRAF: 31;

            then

             A59: (a,x,b) are_collinear by A7, A14, A58, DIRAF: 32;

            

             A60: (a,x,c) are_collinear by A2, DIRAF: 28;

            (a,x,a) are_collinear by A7, A14, A58, DIRAF: 32;

            hence contradiction by A3, A9, A59, A60, DIRAF: 32;

          end;

          

           A61: (b,d,a) are_collinear by A14, DIRAF: 30;

          

           A62: y <> d

          proof

            

             A63: (c,e2,c) are_collinear by DIRAF: 31;

            

             A64: (c,e2,b) are_collinear by A27, DIRAF: 30;

            assume y = d;

            then (c,d,e2) are_collinear by A28, DIRAF: 28;

            then (c,e2,d) are_collinear by DIRAF: 30;

            then (c,e2,a) are_collinear by A7, A14, A64, DIRAF: 35;

            hence contradiction by A3, A31, A64, A63, DIRAF: 32;

          end;

          

           A65: (b,e2,c) are_collinear by A27, DIRAF: 30;

          assume

           A66: not Mid (c,y,b);

          then

           A67: y <> b by DIRAF: 10;

           Mid (b,y,e2) by A28, A30, A66, DIRAF: 11;

          then

          consider z such that

           A68: Mid (b,d,z) and

           A69: (y,d) // (e2,z) by A67, Th20;

          

           A70: (a,e2,a) are_collinear by DIRAF: 31;

           A71:

          now

            assume

             A72: a = z;

             Mid (d,b,a) by A1, DIRAF: 9;

            hence contradiction by A7, A68, A72, DIRAF: 14;

          end;

          (d,y) // (y,x) by A54, DIRAF:def 3;

          then (d,y) // (d,x) by ANALOAF:def 5;

          then (y,d) // (x,d) by DIRAF: 2;

          then (y,d) // (c,e1) by A12, A21, DIRAF: 3;

          then (c,e1) // (e2,z) by A69, A62, ANALOAF:def 5;

          then (a,e2) // (e2,z) by A25, A50, ANALOAF:def 5;

          then Mid (a,e2,z) by DIRAF:def 3;

          then (a,e2,z) are_collinear by DIRAF: 28;

          then

           A73: (a,z,e2) are_collinear by DIRAF: 30;

          

           A74: (b,d,z) are_collinear by A68, DIRAF: 28;

          then

           A75: (a,z,a) are_collinear by A7, A61, DIRAF: 32;

          (b,d,b) are_collinear by DIRAF: 31;

          then (a,z,b) are_collinear by A7, A74, A61, DIRAF: 32;

          then

           A76: (a,e2,b) are_collinear by A73, A75, A71, DIRAF: 32;

          (a,e2,e2) are_collinear by A73, A75, A71, DIRAF: 32;

          then (a,e2,c) are_collinear by A55, A76, A65, DIRAF: 35;

          hence contradiction by A3, A48, A76, A70, DIRAF: 32;

        end;

        then Mid (b,y,c) by DIRAF: 9;

        hence thesis by A53, A32;

      end;

      

       A77: b = d implies Mid (b,d,c) & Mid (x,d,d) by DIRAF: 10;

      

       A78: x = c implies Mid (b,c,c) & Mid (x,c,d) by DIRAF: 10;

      a = x implies Mid (b,b,c) & Mid (x,b,d) by A1, DIRAF: 10;

      hence thesis by A6, A77, A78;

    end;

    theorem :: PASCH:30

    OAS is satisfying_Int_Bet_Pasch by Th29;

    theorem :: PASCH:31

     Mid (p,a,b) & (p,a) // (p9,a9) & not (p,a,p9) are_collinear & (p9,a9,b9) are_collinear & (p,p9) // (a,a9) & (p,p9) // (b,b9) implies Mid (p9,a9,b9)

    proof

      assume that

       A1: Mid (p,a,b) and

       A2: (p,a) // (p9,a9) and

       A3: not (p,a,p9) are_collinear and

       A4: (p9,a9,b9) are_collinear and

       A5: (p,p9) // (a,a9) and

       A6: (p,p9) // (b,b9);

      

       A7: p <> a by A3, DIRAF: 31;

      

       A8: p <> p9 by A3, DIRAF: 31;

      

       A9: (p,a,b) are_collinear by A1, DIRAF: 28;

      then

       A10: (p,b,a) are_collinear by DIRAF: 30;

      now

        

         A11: p <> b by A1, A7, DIRAF: 8;

        

         A12: p9 <> b9

        proof

          assume

           A13: p9 = b9;

          then (b9,p) // (b9,b) by A6, DIRAF: 2;

          then Mid (b9,p,b) or Mid (b9,b,p) by DIRAF: 7;

          then (b9,p,b) are_collinear or (b9,b,p) are_collinear by DIRAF: 28;

          then

           A14: (p,b,b9) are_collinear by DIRAF: 30;

          (p,b,p) are_collinear by DIRAF: 31;

          hence contradiction by A3, A10, A11, A13, A14, DIRAF: 32;

        end;

        

         A15: not (p,a,a9) are_collinear

        proof

          assume

           A16: (p,a,a9) are_collinear ;

          (p,a) '||' (a9,p9) by A2, DIRAF:def 4;

          hence contradiction by A3, A7, A16, DIRAF: 33;

        end;

        then

         A17: a <> a9 by DIRAF: 31;

         A18:

        now

          (a,a9) // (p,p9) by A5, DIRAF: 2;

          then

           A19: (a,a9) '||' (p9,p) by DIRAF:def 4;

          assume (a,a9,p9) are_collinear ;

          then (a,a9,p) are_collinear by A17, A19, DIRAF: 33;

          hence contradiction by A15, DIRAF: 30;

        end;

        assume that

         A20: p9 <> a9 and a9 <> b9;

        consider x such that

         A21: Mid (p,x,b9) and

         A22: (b,b9) // (a,x) by A1, Th19;

         Mid (b9,x,p) by A21, DIRAF: 9;

        then

        consider y such that

         A23: Mid (b9,y,p9) and

         A24: (p,p9) // (x,y) by Th19;

        (b9,y,p9) are_collinear by A23, DIRAF: 28;

        then

         A25: (p9,b9,y) are_collinear by DIRAF: 30;

        

         A26: b <> b9

        proof

          assume b = b9;

          then (a9,p9,b) are_collinear by A4, DIRAF: 30;

          then (a9,p9) '||' (a9,b) by DIRAF:def 5;

          then (a9,p9) // (a9,b) or (a9,p9) // (b,a9) by DIRAF:def 4;

          then (p9,a9) // (a9,b) or (p9,a9) // (b,a9) by DIRAF: 2;

          then (p,a) // (a9,b) or (p,a) // (b,a9) by A2, A20, DIRAF: 3;

          then (p,a) '||' (b,a9) by DIRAF:def 4;

          hence contradiction by A1, A7, A15, DIRAF: 28, DIRAF: 33;

        end;

        

         A27: x <> a

        proof

          assume x = a;

          then

           A28: (p,a,b9) are_collinear by A21, DIRAF: 28;

          (p,a,a) are_collinear by DIRAF: 31;

          then

           A29: (b,b9,a) are_collinear by A7, A9, A28, DIRAF: 32;

          (p,a,p) are_collinear by DIRAF: 31;

          then

           A30: (b,b9,p) are_collinear by A7, A9, A28, DIRAF: 32;

          (b,b9) // (p,p9) by A6, DIRAF: 2;

          then (b,b9) '||' (p,p9) by DIRAF:def 4;

          then (b,b9,p9) are_collinear by A26, A30, DIRAF: 33;

          hence contradiction by A3, A26, A29, A30, DIRAF: 32;

        end;

        

         A31: (p9,b9,a9) are_collinear by A4, DIRAF: 30;

        then

         A32: (y,a9,a9) are_collinear by A12, A25, DIRAF: 32;

        

         A33: (p,p9) // (a,x) by A6, A22, A26, DIRAF: 3;

        then (a,x) // (x,y) by A8, A24, ANALOAF:def 5;

        then (a,x) // (a,y) by ANALOAF:def 5;

        then (p,p9) // (a,y) by A27, A33, DIRAF: 3;

        then (a,y) // (a,a9) by A5, A8, ANALOAF:def 5;

        then (a,y) '||' (a,a9) by DIRAF:def 4;

        then (a,y,a9) are_collinear by DIRAF:def 5;

        then

         A34: (y,a9,a) are_collinear by DIRAF: 30;

        (p9,b9,p9) are_collinear by DIRAF: 31;

        then (y,a9,p9) are_collinear by A12, A25, A31, DIRAF: 32;

        then y = a9 or (a,a9,p9) are_collinear by A34, A32, DIRAF: 32;

        hence thesis by A23, A18, DIRAF: 9;

      end;

      hence thesis by DIRAF: 10;

    end;