hessenbe.miz



    begin

    reserve PCPP for CollProjectiveSpace,

a,a9,a1,a2,a3,b,b9,b1,b2,c,c1,c3,d,d9,e,o,p,p1,p2,p3,r,q,q1,q2,q3,x,y for Element of PCPP;

    theorem :: HESSENBE:1

    

     Th1: (a,b,c) are_collinear implies (b,c,a) are_collinear & (c,a,b) are_collinear & (b,a,c) are_collinear & (a,c,b) are_collinear & (c,b,a) are_collinear

    proof

      assume

       A1: (a,b,c) are_collinear ;

      then (b,a,c) are_collinear by COLLSP: 4;

      then

       A2: (b,c,a) are_collinear by COLLSP: 4;

      (a,c,b) are_collinear by A1, COLLSP: 4;

      hence thesis by A2, COLLSP: 4;

    end;

    theorem :: HESSENBE:2

    

     Th2: a <> b & (a,b,c) are_collinear & (a,b,d) are_collinear implies (a,c,d) are_collinear

    proof

      

       A1: (a,b,a) are_collinear by ANPROJ_2:def 7;

      assume a <> b & (a,b,c) are_collinear & (a,b,d) are_collinear ;

      hence thesis by A1, ANPROJ_2:def 8;

    end;

    theorem :: HESSENBE:3

    p <> q & (a,b,p) are_collinear & (a,b,q) are_collinear & (p,q,r) are_collinear implies (a,b,r) are_collinear

    proof

      assume that

       A1: p <> q and

       A2: (a,b,p) are_collinear & (a,b,q) are_collinear and

       A3: (p,q,r) are_collinear ;

      now

        assume

         A4: a <> b;

        (b,a,p) are_collinear & (b,a,q) are_collinear by A2, Th1;

        then (b,p,q) are_collinear by A4, Th2;

        then

         A5: (p,q,b) are_collinear by Th1;

        (a,p,q) are_collinear by A2, A4, Th2;

        then (p,q,a) are_collinear by Th1;

        hence thesis by A1, A3, A5, ANPROJ_2:def 8;

      end;

      hence thesis by ANPROJ_2:def 7;

    end;

    theorem :: HESSENBE:4

    

     Th4: p <> q implies ex r st not (p,q,r) are_collinear

    proof

      consider a, b, c such that

       A1: not (a,b,c) are_collinear by COLLSP:def 6;

      assume p <> q;

      then (p,q,a) are_collinear & (p,q,b) are_collinear & (p,q,c) are_collinear implies contradiction by A1, ANPROJ_2:def 8;

      hence thesis;

    end;

    theorem :: HESSENBE:5

    ex q, r st not (p,q,r) are_collinear

    proof

      consider q such that

       A1: p <> q and p <> q and (p,p,q) are_collinear by ANPROJ_2:def 10;

      ex r st not (p,q,r) are_collinear by A1, Th4;

      hence thesis;

    end;

    theorem :: HESSENBE:6

    

     Th6: not (a,b,c) are_collinear & (a,b,b9) are_collinear & a <> b9 implies not (a,b9,c) are_collinear

    proof

      assume that

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

       A2: (a,b,b9) are_collinear and

       A3: a <> b9;

      assume

       A4: not thesis;

      (a,b9,b) are_collinear by A2, Th1;

      hence contradiction by A1, A3, A4, Th2;

    end;

    theorem :: HESSENBE:7

    

     Th7: not (a,b,c) are_collinear & (a,b,d) are_collinear & (a,c,d) are_collinear implies a = d

    proof

      assume that

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

       A2: (a,b,d) are_collinear & (a,c,d) are_collinear ;

      assume

       A3: not thesis;

      

       A4: (a,d,a) are_collinear by ANPROJ_2:def 7;

      (a,d,b) are_collinear & (a,d,c) are_collinear by A2, Th1;

      hence contradiction by A1, A3, A4, ANPROJ_2:def 8;

    end;

    theorem :: HESSENBE:8

    

     Th8: not (o,a,d) are_collinear & (o,d,d9) are_collinear & d <> d9 & (a9,d9,x) are_collinear & (o,a,a9) are_collinear & o <> a9 implies x <> d

    proof

      assume that

       A1: not (o,a,d) are_collinear and

       A2: (o,d,d9) are_collinear and

       A3: d <> d9 and

       A4: (a9,d9,x) are_collinear and

       A5: (o,a,a9) are_collinear and

       A6: o <> a9;

      assume not thesis;

      then

       A7: (d,d9,a9) are_collinear by A4, Th1;

      (d,d9,o) are_collinear by A2, Th1;

      then (d,o,a9) are_collinear by A3, A7, Th2;

      then

       A8: (o,a9,d) are_collinear by Th1;

      (o,a9,a) are_collinear by A5, Th1;

      hence contradiction by A1, A6, A8, Th2;

    end;

    theorem :: HESSENBE:9

    

     Th9: not (a1,a2,a3) are_collinear & (a1,a2,c3) are_collinear & (a2,a3,c1) are_collinear & (c1,c3,x) are_collinear & c3 <> a1 & c3 <> a2 & c1 <> a2 & c1 <> a3 implies a1 <> x & a3 <> x

    proof

      assume that

       A1: not (a1,a2,a3) are_collinear and

       A2: (a1,a2,c3) are_collinear and

       A3: (a2,a3,c1) are_collinear and

       A4: (c1,c3,x) are_collinear and

       A5: c3 <> a1 and

       A6: c3 <> a2 and

       A7: c1 <> a2 and

       A8: c1 <> a3;

      

       A9: a3 <> x

      proof

        assume not thesis;

        then

         A10: (a3,c1,c3) are_collinear by A4, Th1;

        (a3,c1,a2) are_collinear by A3, Th1;

        then (a3,a2,c3) are_collinear by A8, A10, Th2;

        then

         A11: (a2,c3,a3) are_collinear by Th1;

        (a2,c3,a1) are_collinear by A2, Th1;

        then (a2,a1,a3) are_collinear by A6, A11, Th2;

        hence contradiction by A1, Th1;

      end;

      a1 <> x

      proof

        assume not thesis;

        then

         A12: (a1,c3,c1) are_collinear by A4, Th1;

        (a1,c3,a2) are_collinear by A2, Th1;

        then (a1,c1,a2) are_collinear by A5, A12, Th2;

        then

         A13: (a2,c1,a1) are_collinear by Th1;

        (a2,c1,a3) are_collinear by A3, Th1;

        then (a2,a1,a3) are_collinear by A7, A13, Th2;

        hence contradiction by A1, Th1;

      end;

      hence thesis by A9;

    end;

    theorem :: HESSENBE:10

    

     Th10: not (a,b,c) are_collinear & (a,b,d) are_collinear & (c,e,d) are_collinear & e <> c & d <> a implies not (e,a,c) are_collinear

    proof

      assume that

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

       A2: (a,b,d) are_collinear and

       A3: (c,e,d) are_collinear & e <> c and

       A4: d <> a;

      assume not thesis;

      then (c,e,a) are_collinear by Th1;

      then (c,a,d) are_collinear by A3, Th2;

      then

       A5: (a,d,c) are_collinear by Th1;

      (a,d,b) are_collinear by A2, Th1;

      hence contradiction by A1, A4, A5, Th2;

    end;

    theorem :: HESSENBE:11

    

     Th11: not (p1,p2,q1) are_collinear & (p1,p2,q2) are_collinear & (q1,q2,q3) are_collinear & q2 <> q3 implies not (p2,p1,q3) are_collinear

    proof

      assume that

       A1: not (p1,p2,q1) are_collinear and

       A2: (p1,p2,q2) are_collinear and

       A3: (q1,q2,q3) are_collinear and

       A4: q2 <> q3;

      

       A5: p1 <> p2 by A1, ANPROJ_2:def 7;

      assume

       A6: not thesis;

      then (p1,p2,q3) are_collinear by Th1;

      then (p1,q2,q3) are_collinear by A2, A5, Th2;

      then

       A7: (q2,q3,p1) are_collinear by Th1;

      (p2,p1,q2) are_collinear by A2, Th1;

      then (p2,q2,q3) are_collinear by A6, A5, Th2;

      then

       A8: (q2,q3,p2) are_collinear by Th1;

      (q2,q3,q1) are_collinear by A3, Th1;

      hence contradiction by A1, A4, A7, A8, ANPROJ_2:def 8;

    end;

    theorem :: HESSENBE:12

     not (p1,p2,q1) are_collinear & (p1,p2,p3) are_collinear & (q1,q2,p3) are_collinear & p3 <> q2 & p2 <> p3 implies not (p3,p2,q2) are_collinear

    proof

      assume that

       A1: not (p1,p2,q1) are_collinear and

       A2: (p1,p2,p3) are_collinear and

       A3: (q1,q2,p3) are_collinear and

       A4: p3 <> q2 and

       A5: p2 <> p3;

      assume

       A6: not thesis;

      (p3,p2,p1) are_collinear by A2, Th1;

      then

       A7: (p3,q2,p1) are_collinear by A5, A6, Th2;

      

       A8: (p3,q2,q1) are_collinear by A3, Th1;

      (p3,q2,p2) are_collinear by A6, Th1;

      hence contradiction by A1, A4, A7, A8, ANPROJ_2:def 8;

    end;

    theorem :: HESSENBE:13

    

     Th13: not (p1,p2,q1) are_collinear & (p1,p2,p3) are_collinear & (q1,q2,p1) are_collinear & p1 <> p3 & p1 <> q2 implies not (p3,p1,q2) are_collinear

    proof

      assume that

       A1: not (p1,p2,q1) are_collinear and

       A2: (p1,p2,p3) are_collinear and

       A3: (q1,q2,p1) are_collinear and

       A4: p1 <> p3 and

       A5: p1 <> q2;

      

       A6: (p1,q2,q1) are_collinear by A3, Th1;

      assume not thesis;

      then

       A7: (p1,p3,q2) are_collinear by Th1;

      (p1,p3,p2) are_collinear by A2, Th1;

      then (p1,q2,p2) are_collinear by A4, A7, Th2;

      hence contradiction by A1, A5, A6, Th2;

    end;

    theorem :: HESSENBE:14

    

     Th14: a1 <> a2 & b1 <> b2 & (b1,b2,x) are_collinear & (b1,b2,y) are_collinear & (a1,a2,x) are_collinear & (a1,a2,y) are_collinear & not (a1,a2,b1) are_collinear implies x = y

    proof

      assume that

       A1: a1 <> a2 and

       A2: b1 <> b2 & (b1,b2,x) are_collinear & (b1,b2,y) are_collinear and

       A3: (a1,a2,x) are_collinear & (a1,a2,y) are_collinear and

       A4: not (a1,a2,b1) are_collinear ;

      (a1,a2,a2) are_collinear by ANPROJ_2:def 7;

      then

       A5: (x,y,a2) are_collinear by A1, A3, ANPROJ_2:def 8;

      (b1,b2,b1) are_collinear by ANPROJ_2:def 7;

      then

       A6: (x,y,b1) are_collinear by A2, ANPROJ_2:def 8;

      assume

       A7: not thesis;

      (a1,a2,a1) are_collinear by ANPROJ_2:def 7;

      then (x,y,a1) are_collinear by A1, A3, ANPROJ_2:def 8;

      hence contradiction by A4, A7, A6, A5, ANPROJ_2:def 8;

    end;

    theorem :: HESSENBE:15

    

     Th15: not (o,a1,a2) are_collinear & (o,a1,b1) are_collinear & (o,a2,b2) are_collinear & o <> b1 & o <> b2 implies not (o,b1,b2) are_collinear

    proof

      assume that

       A1: ( not (o,a1,a2) are_collinear ) & (o,a1,b1) are_collinear and

       A2: (o,a2,b2) are_collinear and

       A3: o <> b1 and

       A4: o <> b2;

       not (o,b1,a2) are_collinear by A1, A3, Th6;

      then not (o,a2,b1) are_collinear by Th1;

      then not (o,b2,b1) are_collinear by A2, A4, Th6;

      hence thesis by Th1;

    end;

    reserve PCPP for Pappian CollProjectivePlane,

a,a1,a2,a3,b1,b2,b3,c1,c2,c3,o,p,p1,p2,p3,q,q9,q1,q2,q3,r,r1,r2,r3,x,y,z for Element of PCPP;

    theorem :: HESSENBE:16

    

     Th16: p2 <> p3 & p1 <> p3 & q2 <> q3 & q1 <> q2 & q1 <> q3 & not (p1,p2,q1) are_collinear & (p1,p2,p3) are_collinear & (q1,q2,q3) are_collinear & (p1,q2,r3) are_collinear & (q1,p2,r3) are_collinear & (p1,q3,r2) are_collinear & (p3,q1,r2) are_collinear & (p2,q3,r1) are_collinear & (p3,q2,r1) are_collinear implies (r1,r2,r3) are_collinear

    proof

      assume that

       A1: p2 <> p3 and

       A2: p1 <> p3 and

       A3: q2 <> q3 and

       A4: q1 <> q2 and

       A5: q1 <> q3 and

       A6: not (p1,p2,q1) are_collinear and

       A7: (p1,p2,p3) are_collinear and

       A8: (q1,q2,q3) are_collinear and

       A9: (p1,q2,r3) are_collinear and

       A10: (q1,p2,r3) are_collinear and

       A11: (p1,q3,r2) are_collinear and

       A12: (p3,q1,r2) are_collinear and

       A13: (p2,q3,r1) are_collinear and

       A14: (p3,q2,r1) are_collinear ;

      

       A15: p1 <> p2 by A6, ANPROJ_2:def 7;

       A16:

      now

        assume

         A17: not (p1,p2,q2) are_collinear ;

         A18:

        now

          assume

           A19: not (p1,p2,q3) are_collinear ;

           A20:

          now

             A21:

            now

              ( not (p2,p1,q2) are_collinear ) & (p2,p1,p3) are_collinear by A7, A17, Th1;

              then not (p2,p3,q2) are_collinear by A1, Th6;

              then

               A22: not (q2,p2,p3) are_collinear by Th1;

              assume

               A23: (q1,q2,p2) are_collinear ;

              then

               A24: (p2,q1,q2) are_collinear by Th1;

              p2 <> q1 & (p2,q1,r3) are_collinear by A6, A10, Th1, ANPROJ_2:def 7;

              then (p2,r3,q2) are_collinear by A24, Th2;

              then

               A25: (q2,p2,r3) are_collinear by Th1;

              (q2,p1,r3) are_collinear & not (q2,p1,p2) are_collinear by A9, A17, Th1;

              then

               A26: q2 = r3 by A25, Th7;

              

               A27: (q2,q1,q3) are_collinear by A8, Th1;

              (q2,q1,p2) are_collinear by A23, Th1;

              then (q2,p2,q3) are_collinear by A4, A27, Th2;

              then

               A28: (p2,q3,q2) are_collinear by Th1;

              p2 <> q3 by A19, ANPROJ_2:def 7;

              then (p2,r1,q2) are_collinear by A13, A28, Th2;

              then

               A29: (q2,p2,r1) are_collinear by Th1;

              (q2,p3,r1) are_collinear by A14, Th1;

              then q2 = r1 by A29, A22, Th7;

              hence thesis by A26, ANPROJ_2:def 7;

            end;

             A30:

            now

              ( not (p2,p1,q3) are_collinear ) & (p2,p1,p3) are_collinear by A7, A19, Th1;

              then not (p2,p3,q3) are_collinear by A1, Th6;

              then

               A31: not (q3,p2,p3) are_collinear by Th1;

              assume

               A32: (q1,q2,p3) are_collinear ;

              then

               A33: (q2,q1,p3) are_collinear by Th1;

              (q2,q1,q3) are_collinear by A8, Th1;

              then (q2,q3,p3) are_collinear by A4, A33, Th2;

              then (p3,q2,q3) are_collinear by Th1;

              then (p3,r1,q3) are_collinear by A7, A14, A17, Th2;

              then

               A34: (q3,p3,r1) are_collinear by Th1;

               not (p1,p3,q3) are_collinear by A2, A7, A19, Th6;

              then

               A35: not (q3,p1,p3) are_collinear by Th1;

              (q1,q3,p3) are_collinear by A4, A8, A32, Th2;

              then (p3,q1,q3) are_collinear by Th1;

              then (p3,r2,q3) are_collinear by A6, A7, A12, Th2;

              then

               A36: (q3,p3,r2) are_collinear by Th1;

              (q3,p2,r1) are_collinear by A13, Th1;

              then

               A37: q3 = r1 by A34, A31, Th7;

              (q3,p1,r2) are_collinear by A11, Th1;

              then q3 = r2 by A36, A35, Th7;

              hence thesis by A37, ANPROJ_2:def 7;

            end;

             A38:

            now

               not (p1,p3,q1) are_collinear by A2, A6, A7, Th6;

              then

               A39: not (q1,p1,p3) are_collinear by Th1;

              assume

               A40: (q1,q2,p1) are_collinear ;

              then (q1,p1,q3) are_collinear by A4, A8, Th2;

              then

               A41: (p1,q3,q1) are_collinear by Th1;

              p1 <> q3 by A19, ANPROJ_2:def 7;

              then (p1,r2,q1) are_collinear by A11, A41, Th2;

              then

               A42: (q1,p1,r2) are_collinear by Th1;

              

               A43: p1 <> q2 by A17, ANPROJ_2:def 7;

              (p1,q2,q1) are_collinear by A40, Th1;

              then (p1,r3,q1) are_collinear by A9, A43, Th2;

              then

               A44: (q1,p1,r3) are_collinear by Th1;

               not (q1,p2,p1) are_collinear by A6, Th1;

              then

               A45: q1 = r3 by A10, A44, Th7;

              (q1,p3,r2) are_collinear by A12, Th1;

              then q1 = r2 by A42, A39, Th7;

              hence thesis by A45, ANPROJ_2:def 7;

            end;

            assume (q1,q2,p1) are_collinear or (q1,q2,p2) are_collinear or (q1,q2,p3) are_collinear ;

            hence thesis by A38, A21, A30;

          end;

          now

            assume that

             A46: not (q1,q2,p1) are_collinear and

             A47: ( not (q1,q2,p2) are_collinear ) & not (q1,q2,p3) are_collinear ;

            consider o such that

             A48: (p1,p2,o) are_collinear and

             A49: (q1,q2,o) are_collinear by ANPROJ_2:def 14;

             not (p1,o,q1) are_collinear by A6, A46, A48, A49, Th6;

            then

             A50: not (o,p1,q1) are_collinear by Th1;

            (q1,q3,o) are_collinear by A4, A8, A49, Th2;

            then

             A51: (o,q1,q3) are_collinear by Th1;

            (p1,p3,o) are_collinear by A7, A15, A48, Th2;

            then

             A52: (o,p1,p3) are_collinear by Th1;

            (o,p1,p2) are_collinear & (o,q1,q2) are_collinear by A48, A49, Th1;

            hence thesis by A1, A2, A3, A4, A5, A9, A10, A11, A12, A13, A14, A15, A17, A19, A47, A48, A49, A52, A51, A50, ANPROJ_2:def 13;

          end;

          hence thesis by A20;

        end;

        now

          assume

           A53: (p1,p2,q3) are_collinear ;

           A54:

          now

            assume that

             A55: p2 <> q3 and

             A56: p1 <> q3;

            (p1,q3,p2) are_collinear by A53, Th1;

            then (p1,p2,r2) are_collinear by A11, A56, Th2;

            then (p1,r2,p3) are_collinear by A7, A15, Th2;

            then

             A57: (p3,p1,r2) are_collinear by Th1;

             not (p1,p3,q1) are_collinear by A2, A6, A7, Th6;

            then not (p3,q1,p1) are_collinear by Th1;

            then

             A58: p3 = r2 by A12, A57, Th7;

            

             A59: (p2,p1,p3) are_collinear by A7, Th1;

            (p2,q3,p1) are_collinear by A53, Th1;

            then (p2,p1,r1) are_collinear by A13, A55, Th2;

            then (p2,r1,p3) are_collinear by A15, A59, Th2;

            then

             A60: (p3,p2,r1) are_collinear by Th1;

            ( not (p2,p1,q2) are_collinear ) & (p2,p1,p3) are_collinear by A7, A17, Th1;

            then not (p2,p3,q2) are_collinear by A1, Th6;

            then not (p3,q2,p2) are_collinear by Th1;

            then p3 = r1 by A14, A60, Th7;

            hence thesis by A58, ANPROJ_2:def 7;

          end;

           A61:

          now

             not (p1,p3,q1) are_collinear by A2, A6, A7, Th6;

            then

             A62: not (p3,p1,q1) are_collinear by Th1;

            

             A63: not (p2,q1,p1) are_collinear by A6, Th1;

            

             A64: (p2,q1,r3) are_collinear by A10, Th1;

            assume

             A65: p2 = q3;

            then (p2,q1,q2) are_collinear by A8, Th1;

            then (p2,q2,r3) are_collinear by A5, A65, A64, Th2;

            then

             A66: (q2,p2,r3) are_collinear by Th1;

            (p2,q1,q2) are_collinear by A8, A65, Th1;

            then not (p2,q2,p1) are_collinear by A3, A65, A63, Th6;

            then

             A67: not (q2,p1,p2) are_collinear by Th1;

            (p1,p3,r2) are_collinear by A7, A11, A15, A65, Th2;

            then (p3,p1,r2) are_collinear by Th1;

            then

             A68: p3 = r2 by A12, A62, Th7;

            (q2,p1,r3) are_collinear by A9, Th1;

            then q2 = r3 by A66, A67, Th7;

            hence thesis by A14, A68, Th1;

          end;

          now

            assume

             A69: p1 = q3;

            then (p1,p2,r1) are_collinear by A13, Th1;

            then (p1,p3,r1) are_collinear by A7, A15, Th2;

            then

             A70: (p3,p1,r1) are_collinear by Th1;

            (p1,q2,q1) are_collinear by A8, A69, Th1;

            then (p1,q1,r3) are_collinear by A3, A9, A69, Th2;

            then

             A71: (q1,p1,r3) are_collinear by Th1;

             not (p3,p1,q2) are_collinear by A2, A3, A6, A7, A8, A69, Th13;

            then

             A72: p3 = r1 by A14, A70, Th7;

             not (q1,p1,p2) are_collinear by A6, Th1;

            then q1 = r3 by A10, A71, Th7;

            hence thesis by A12, A72, Th1;

          end;

          hence thesis by A61, A54;

        end;

        hence thesis by A18;

      end;

      now

         A73:

        now

           not (p1,p3,q1) are_collinear by A2, A6, A7, Th6;

          then

           A74: not (q1,p1,p3) are_collinear by Th1;

          

           A75: not (p1,q1,p2) are_collinear by A6, Th1;

          assume

           A76: p1 = q2;

          then (p1,q3,q1) are_collinear by A8, Th1;

          then (p1,q1,r2) are_collinear by A3, A11, A76, Th2;

          then

           A77: (q1,p1,r2) are_collinear by Th1;

          

           A78: (p1,p3,p2) are_collinear by A7, Th1;

          (p1,p3,r1) are_collinear by A14, A76, Th1;

          then (p1,p2,r1) are_collinear by A2, A78, Th2;

          then

           A79: (p2,p1,r1) are_collinear by Th1;

          (q1,p3,r2) are_collinear by A12, Th1;

          then

           A80: q1 = r2 by A77, A74, Th7;

          (p1,q1,q3) are_collinear by A8, A76, Th1;

          then not (p1,q3,p2) are_collinear by A3, A76, A75, Th6;

          then not (p2,p1,q3) are_collinear by Th1;

          then r1 = p2 by A13, A79, Th7;

          hence thesis by A10, A80, Th1;

        end;

        assume

         A81: (p1,p2,q2) are_collinear ;

         A82:

        now

          assume that

           A83: p1 <> q2 and

           A84: p3 <> q2;

          (p1,q2,p2) are_collinear by A81, Th1;

          then (p1,p2,r3) are_collinear by A9, A83, Th2;

          then

           A85: (p2,p1,r3) are_collinear by Th1;

          (p1,q2,p3) are_collinear by A7, A15, A81, Th2;

          then (p3,q2,p1) are_collinear by Th1;

          then (p3,p1,r1) are_collinear by A14, A84, Th2;

          then

           A86: (p1,p3,r1) are_collinear by Th1;

          (p1,p3,p2) are_collinear by A7, Th1;

          then (p1,p2,r1) are_collinear by A2, A86, Th2;

          then

           A87: (p2,p1,r1) are_collinear by Th1;

           not (p2,p1,q3) are_collinear by A3, A6, A8, A81, Th11;

          then

           A88: p2 = r1 by A13, A87, Th7;

          ( not (p2,p1,q1) are_collinear ) & (p2,q1,r3) are_collinear by A6, A10, Th1;

          then p2 = r3 by A85, Th7;

          hence thesis by A88, ANPROJ_2:def 7;

        end;

        now

          assume

           A89: p3 = q2;

          then (q1,q3,p3) are_collinear by A8, Th1;

          then

           A90: not (q3,p1,q1) are_collinear by A2, A5, A6, A7, Th10;

          (p1,p3,p2) are_collinear by A7, Th1;

          then (p1,p2,r3) are_collinear by A2, A9, A89, Th2;

          then

           A91: (p2,p1,r3) are_collinear by Th1;

          ( not (p2,p1,q1) are_collinear ) & (p2,q1,r3) are_collinear by A6, A10, Th1;

          then

           A92: p2 = r3 by A91, Th7;

          (q1,q2,r2) are_collinear by A12, A89, Th1;

          then (q1,q3,r2) are_collinear by A4, A8, Th2;

          then

           A93: (q3,q1,r2) are_collinear by Th1;

          (q3,p1,r2) are_collinear by A11, Th1;

          then (r3,r2,r1) are_collinear by A13, A92, A90, A93, Th7;

          hence thesis by Th1;

        end;

        hence thesis by A73, A82;

      end;

      hence thesis by A16;

    end;

    

     Lm1: o <> b1 & o <> b2 & not (o,a1,a2) are_collinear & not (o,a1,a3) are_collinear & not (o,a2,a3) are_collinear & (a1,a2,c3) are_collinear & (b1,b2,c3) are_collinear & (a2,a3,c1) are_collinear & (b2,b3,c1) are_collinear & (a1,a3,c2) are_collinear & (b1,b3,c2) are_collinear & (o,a1,b1) are_collinear & (o,a2,b2) are_collinear & (o,a3,b3) are_collinear & ((a1,a2,a3) are_collinear or (b1,b2,b3) are_collinear ) implies (c1,c2,c3) are_collinear

    proof

      assume that

       A1: o <> b1 and

       A2: o <> b2 and

       A3: not (o,a1,a2) are_collinear and

       A4: not (o,a1,a3) are_collinear and

       A5: not (o,a2,a3) are_collinear and

       A6: (a1,a2,c3) are_collinear and

       A7: (b1,b2,c3) are_collinear and

       A8: (a2,a3,c1) are_collinear and

       A9: (b2,b3,c1) are_collinear and

       A10: (a1,a3,c2) are_collinear and

       A11: (b1,b3,c2) are_collinear and

       A12: (o,a1,b1) are_collinear and

       A13: (o,a2,b2) are_collinear and

       A14: (o,a3,b3) are_collinear and

       A15: (a1,a2,a3) are_collinear or (b1,b2,b3) are_collinear ;

      

       A16: a1 <> a3 by A4, ANPROJ_2:def 7;

      

       A17: a2 <> a3 by A5, ANPROJ_2:def 7;

      

       A18: a1 <> a2 by A3, ANPROJ_2:def 7;

       A19:

      now

        assume

         A20: (a1,a2,a3) are_collinear ;

        then (a2,a3,a1) are_collinear by Th1;

        then (a2,a1,c1) are_collinear by A8, A17, Th2;

        then

         A21: (a1,a2,c1) are_collinear by Th1;

        (a1,a3,a2) are_collinear by A20, Th1;

        then (a1,a2,c2) are_collinear by A10, A16, Th2;

        hence thesis by A6, A18, A21, ANPROJ_2:def 8;

      end;

      

       A22: b2 <> b3 by A2, A5, A13, A14, Th7;

      

       A23: b1 <> b3 by A1, A4, A12, A14, Th7;

      

       A24: b1 <> b2 by A1, A3, A12, A13, Th7;

      now

        assume

         A25: (b1,b2,b3) are_collinear ;

        then (b2,b3,b1) are_collinear by Th1;

        then (b2,b1,c1) are_collinear by A9, A22, Th2;

        then

         A26: (b1,b2,c1) are_collinear by Th1;

        (b1,b3,b2) are_collinear by A25, Th1;

        then (b1,b2,c2) are_collinear by A11, A23, Th2;

        hence thesis by A7, A24, A26, ANPROJ_2:def 8;

      end;

      hence thesis by A15, A19;

    end;

    

     Lm2: o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not (o,a1,a2) are_collinear & not (o,a1,a3) are_collinear & not (o,a2,a3) are_collinear & not (o,c1,c3) are_collinear & (a1,a2,c3) are_collinear & (b1,b2,c3) are_collinear & (a2,a3,c1) are_collinear & (b2,b3,c1) are_collinear & (a1,a3,c2) are_collinear & (b1,b3,c2) are_collinear & (o,a1,b1) are_collinear & (o,a2,b2) are_collinear & (o,a3,b3) are_collinear & (o,a2,x) are_collinear & (a1,a3,x) are_collinear & not (c1,c3,x) are_collinear implies (c1,c2,c3) are_collinear

    proof

      assume that

       A1: o <> b1 and

       A2: a1 <> b1 and

       A3: o <> b2 and

       A4: a2 <> b2 and

       A5: o <> b3 and

       A6: a3 <> b3 and

       A7: not (o,a1,a2) are_collinear and

       A8: not (o,a1,a3) are_collinear and

       A9: not (o,a2,a3) are_collinear and

       A10: not (o,c1,c3) are_collinear and

       A11: (a1,a2,c3) are_collinear and

       A12: (b1,b2,c3) are_collinear and

       A13: (a2,a3,c1) are_collinear and

       A14: (b2,b3,c1) are_collinear and

       A15: (a1,a3,c2) are_collinear and

       A16: (b1,b3,c2) are_collinear and

       A17: (o,a1,b1) are_collinear and

       A18: (o,a2,b2) are_collinear and

       A19: (o,a3,b3) are_collinear and

       A20: (o,a2,x) are_collinear and

       A21: (a1,a3,x) are_collinear and

       A22: not (c1,c3,x) are_collinear ;

      

       A23: o <> a1 by A7, ANPROJ_2:def 7;

      

       A24: b1 <> b3 by A1, A8, A17, A19, Th7;

      

       A25: a1 <> a2 by A7, ANPROJ_2:def 7;

      

       A26: o <> a2 by A7, ANPROJ_2:def 7;

      

       A27: o <> a3 by A8, ANPROJ_2:def 7;

      

       A28: a1 <> a3 by A8, ANPROJ_2:def 7;

      

       A29: a2 <> a3 by A9, ANPROJ_2:def 7;

      ( not (a1,o,a3) are_collinear ) & (a1,o,b1) are_collinear by A8, A17, Th1;

      then not (a1,b1,a3) are_collinear by A2, Th6;

      then

       A30: not (a1,a3,b1) are_collinear by Th1;

       A31:

      now

        ( not (o,a2,a1) are_collinear ) & (b2,b1,c3) are_collinear by A7, A12, Th1;

        then

         A32: a1 <> c3 by A2, A3, A17, A18, Th8;

         not (a1,a2,o) are_collinear by A7, Th1;

        then not (a1,c3,o) are_collinear by A11, A32, Th6;

        then

         A33: not (o,a1,c3) are_collinear by Th1;

        

         A34: c1 <> c3 by A10, ANPROJ_2:def 7;

        o <> x by A8, A21, Th1;

        then not (o,x,a3) are_collinear by A9, A20, Th6;

        then

         A35: not (x,a3,o) are_collinear by Th1;

        

         A36: a1 <> a3 by A8, ANPROJ_2:def 7;

        ( not (o,a2,a1) are_collinear ) & (b2,b1,c3) are_collinear by A7, A12, Th1;

        then

         A37: a1 <> c3 by A2, A3, A17, A18, Th8;

        

         A38: (a2,a1,c3) are_collinear by A11, Th1;

        

         A39: (a2,a1,c3) are_collinear by A11, Th1;

        

         A40: a2 <> c3 by A1, A4, A7, A12, A17, A18, Th8;

         not (o,b2,a3) are_collinear by A3, A9, A18, Th6;

        then

         A41: not (a3,o,b2) are_collinear by Th1;

        

         A42: c1 <> c3 by A10, ANPROJ_2:def 7;

        

         A43: (o,b1,a1) are_collinear by A17, Th1;

        

         A44: not (a1,a3,o) are_collinear by A8, Th1;

        ( not (o,a3,a2) are_collinear ) & (b3,b2,c1) are_collinear by A9, A14, Th1;

        then

         A45: a2 <> c1 by A4, A5, A18, A19, Th8;

        (a3,b3,o) are_collinear by A19, Th1;

        then not (b2,o,b3) are_collinear by A3, A5, A9, A18, Th13;

        then

         A46: not (o,b3,b2) are_collinear by Th1;

        

         A47: o <> a2 by A7, ANPROJ_2:def 7;

        assume that

         A48: not (a1,a2,a3) are_collinear and

         A49: not (b1,b2,b3) are_collinear ;

        

         A50: b1 <> b3 by A49, ANPROJ_2:def 7;

        consider z such that

         A51: (a1,a3,z) are_collinear and

         A52: (c1,c3,z) are_collinear by ANPROJ_2:def 14;

        consider p such that

         A53: (o,z,p) are_collinear and

         A54: (a2,a3,p) are_collinear by ANPROJ_2:def 14;

        

         A55: o <> p by A9, A54, Th1;

        

         A56: a3 <> c1 by A3, A6, A9, A14, A18, A19, Th8;

        then

         A57: a1 <> z by A11, A13, A48, A52, A40, A45, A37, Th9;

        

         A58: a3 <> z by A11, A13, A48, A52, A40, A45, A37, A56, Th9;

        

         A59: a3 <> p

        proof

          assume not thesis;

          then

           A60: (a3,o,z) are_collinear by A53, Th1;

          (a3,a1,z) are_collinear & not (a3,o,a1) are_collinear by A8, A51, Th1;

          hence contradiction by A58, A60, Th7;

        end;

        

         A61: (a3,a1,x) are_collinear by A21, Th1;

        

         A62: (o,b2,a2) are_collinear by A18, Th1;

        a1 <> z by A11, A13, A48, A52, A40, A45, A37, A56, Th9;

        then not (a1,z,o) are_collinear by A51, A44, Th6;

        then not (o,z,a1) are_collinear by Th1;

        then not (o,p,a1) are_collinear by A53, A55, Th6;

        then

         A63: not (o,a1,p) are_collinear by Th1;

        

         A64: (a3,z,a1) are_collinear by A51, Th1;

        

         A65: (p,a2,a3) are_collinear by A54, Th1;

        consider q such that

         A66: (o,a1,q) are_collinear and

         A67: (p,c3,q) are_collinear by ANPROJ_2:def 14;

        consider r such that

         A68: (p,b2,r) are_collinear and

         A69: (q,a3,r) are_collinear by ANPROJ_2:def 14;

        

         A70: (a3,q,r) are_collinear by A69, Th1;

        (o,b3,a3) are_collinear & (a3,a2,c1) are_collinear by A13, A19, Th1;

        then

         A71: b2 <> c1 by A4, A27, A62, A46, Th8;

        

         A72: a2 <> c3 by A1, A4, A7, A12, A17, A18, Th8;

         not (a1,a3,o) are_collinear by A8, Th1;

        then not (a1,z,o) are_collinear by A51, A57, Th6;

        then not (o,z,a1) are_collinear by Th1;

        then not (o,p,a1) are_collinear by A53, A55, Th6;

        then

         A73: b1 <> p by A17, Th1;

        consider a such that

         A74: (c1,c3,a) are_collinear and

         A75: (o,a2,a) are_collinear by ANPROJ_2:def 14;

        

         A76: (c3,c1,a) are_collinear by A74, Th1;

        

         A77: (a,o,a2) are_collinear by A75, Th1;

        

         A78: o <> a by A10, A74, Th1;

        

         A79: c1 <> c3 by A10, ANPROJ_2:def 7;

        

         A80: a2 <> a

        proof

          

           A81: (c3,a2,a1) are_collinear by A11, Th1;

          assume

           A82: not thesis;

          then (c3,a2,c1) are_collinear by A74, Th1;

          then (c3,c1,a1) are_collinear by A40, A81, Th2;

          then

           A83: (c1,c3,a1) are_collinear by Th1;

          

           A84: (c1,a2,a3) are_collinear by A13, Th1;

          (c1,a2,c3) are_collinear by A74, A82, Th1;

          then (c1,c3,a3) are_collinear by A45, A84, Th2;

          hence contradiction by A48, A74, A79, A82, A83, ANPROJ_2:def 8;

        end;

        assume

         A85: not thesis;

        (c3,c1,z) are_collinear by A52, Th1;

        then (c3,a,z) are_collinear by A76, A42, Th2;

        then

         A86: (a,z,c3) are_collinear by Th1;

        

         A87: (o,x,a) are_collinear by A20, A26, A75, Th2;

        consider q9 such that

         A88: (o,a1,q9) are_collinear & (a,a3,q9) are_collinear by ANPROJ_2:def 14;

        (a3,a2,p) are_collinear by A54, Th1;

        then (c3,q9,p) are_collinear by A9, A53, A75, A88, A80, A78, A36, A57, A58, A64, A39, A86, Th16;

        then

         A89: (p,c3,q9) are_collinear by Th1;

         not (a2,a1,a3) are_collinear by A48, Th1;

        then not (a2,c3,a3) are_collinear by A72, A38, Th6;

        then p <> c3 by A54, Th1;

        then

         A90: (a,a3,q) are_collinear by A23, A66, A67, A88, A89, A63, Th14;

        then (a3,q,a) are_collinear by Th1;

        then

         A91: (a3,r,a) are_collinear by A8, A66, A70, Th2;

        ( not (o,a3,a2) are_collinear ) & (b3,b2,c1) are_collinear by A9, A14, Th1;

        then

         A92: a2 <> c1 by A4, A5, A18, A19, Th8;

        

         A93: a <> a2

        proof

          

           A94: (c3,a2,a1) are_collinear by A11, Th1;

          assume

           A95: not thesis;

          then (c3,a2,c1) are_collinear by A74, Th1;

          then (c3,c1,a1) are_collinear by A72, A94, Th2;

          then

           A96: (c1,c3,a1) are_collinear by Th1;

          

           A97: (c1,a2,a3) are_collinear by A13, Th1;

          (c1,a2,c3) are_collinear by A74, A95, Th1;

          then (c1,c3,a3) are_collinear by A92, A97, Th2;

          hence contradiction by A48, A74, A34, A95, A96, ANPROJ_2:def 8;

        end;

        consider z99 be Element of PCPP such that

         A98: (b3,r,z99) are_collinear & (o,p,z99) are_collinear by ANPROJ_2:def 14;

        (a2,b2,o) are_collinear by A18, Th1;

        then

         A99: not (b1,o,b2) are_collinear by A1, A3, A7, A17, Th13;

        then not (o,b1,b2) are_collinear by Th1;

        then

         A100: b2 <> c3 by A4, A11, A23, A43, A62, Th8;

        

         A101: a <> b2

        proof

          

           A102: (c3,b2,b1) are_collinear by A12, Th1;

          assume

           A103: not thesis;

          then (c3,b2,c1) are_collinear by A74, Th1;

          then (c3,c1,b1) are_collinear by A100, A102, Th2;

          then

           A104: (c1,c3,b1) are_collinear by Th1;

          

           A105: (c1,b2,b3) are_collinear by A14, Th1;

          (c1,b2,c3) are_collinear by A74, A103, Th1;

          then (c1,c3,b3) are_collinear by A71, A105, Th2;

          hence contradiction by A49, A74, A34, A103, A104, ANPROJ_2:def 8;

        end;

         not (a2,a3,o) are_collinear by A9, Th1;

        then not (a2,c1,o) are_collinear by A13, A92, Th6;

        then

         A106: a <> c1 by A75, Th1;

        ( not (a2,a1,o) are_collinear ) & (a2,a1,c3) are_collinear by A7, A11, Th1;

        then not (a2,c3,o) are_collinear by A72, Th6;

        then

         A107: a <> c3 by A75, Th1;

        (o,a,b2) are_collinear by A18, A26, A75, Th2;

        then

         A108: (a,o,b2) are_collinear by Th1;

        (a2,o,b2) are_collinear & not (a2,o,a3) are_collinear by A9, A18, Th1;

        then

         A109: not (a2,b2,a3) are_collinear by A4, Th6;

        then

         A110: b2 <> p by A54, Th1;

        (a3,a1,z) are_collinear by A51, Th1;

        then (a3,x,z) are_collinear by A36, A61, Th2;

        then (x,a3,z) are_collinear by Th1;

        then not (x,z,o) are_collinear by A22, A52, A35, Th6;

        then not (o,z,x) are_collinear by Th1;

        then not (o,p,x) are_collinear by A53, A55, Th6;

        then not (o,x,p) are_collinear by Th1;

        then

         A111: not (o,a,p) are_collinear by A78, A87, Th6;

        then not (a,o,p) are_collinear by Th1;

        then not (a,a2,p) are_collinear by A93, A77, Th6;

        then not (p,a2,a) are_collinear by Th1;

        then

         A112: not (p,a3,a) are_collinear by A59, A65, Th6;

        then

         A113: p <> r by A91, Th1;

        (o,a,b2) are_collinear by A18, A26, A75, Th2;

        then not (o,b2,p) are_collinear by A3, A111, Th6;

        then not (p,b2,o) are_collinear by Th1;

        then not (p,r,o) are_collinear by A68, A113, Th6;

        then

         A114: z <> r by A53, Th1;

        consider z9 be Element of PCPP such that

         A115: (b1,r,z9) are_collinear & (o,p,z9) are_collinear by ANPROJ_2:def 14;

        

         A116: not (o,a,a3) are_collinear by A9, A75, A78, Th6;

        then not (a,o,a3) are_collinear by Th1;

        then

         A117: not (a,b2,a3) are_collinear by A101, A108, Th6;

        then

         A118: b2 <> r by A91, Th1;

         A119:

        now

          (o,b1,q) are_collinear by A17, A23, A66, Th2;

          then

           A120: (b1,o,q) are_collinear by Th1;

          assume b1 <> q;

          then not (b1,q,b2) are_collinear by A99, A120, Th6;

          then

           A121: not (q,b1,b2) are_collinear by Th1;

          

           A122: (b2,p,r) are_collinear & (q,p,c3) are_collinear by A67, A68, Th1;

          (o,b1,q) are_collinear by A17, A23, A66, Th2;

          then

           A123: (q,b1,o) are_collinear by Th1;

          

           A124: q <> o & b2 <> p by A54, A116, A109, A90, Th1;

          (c3,c1,z) are_collinear & (c3,c1,a) are_collinear by A52, A74, Th1;

          then (c3,z,a) are_collinear by A34, Th2;

          then

           A125: (a,c3,z) are_collinear by Th1;

          

           A126: ( not (c1,c3,o) are_collinear ) & (o,p,z) are_collinear by A10, A53, Th1;

          (a3,a2,c1) are_collinear & (a3,a2,p) are_collinear by A13, A54, Th1;

          then

           A127: (a3,p,c1) are_collinear by A29, Th2;

          (o,a,b2) are_collinear by A18, A26, A75, Th2;

          then

           A128: (b2,o,a) are_collinear by Th1;

          (q,a3,a) are_collinear by A90, Th1;

          then

           A129: (q,r,a) are_collinear by A8, A66, A69, Th2;

          

           A130: b2 <> r & p <> r by A117, A91, A112, Th1;

          (b2,b1,c3) are_collinear & (o,b2,a) are_collinear by A12, A18, A26, A75, Th1, Th2;

          then (z9,a,c3) are_collinear by A1, A115, A124, A130, A121, A123, A122, A129, Th16;

          then

           A131: (a,c3,z9) are_collinear by Th1;

          

           A132: (b3,b2,c1) are_collinear by A14, Th1;

          (a3,o,b3) are_collinear & (b2,r,p) are_collinear by A19, A68, Th1;

          then (z99,c1,a) are_collinear by A5, A6, A98, A110, A91, A118, A41, A113, A128, A127, A132, Th16;

          then

           A133: (c1,a,z99) are_collinear by Th1;

          (c1,a,c3) are_collinear by A74, Th1;

          then (c1,c3,z99) are_collinear by A106, A133, Th2;

          then (b3,r,z) are_collinear by A52, A98, A34, A55, A126, Th14;

          then

           A134: (z,r,b3) are_collinear by Th1;

          (o,p,z) are_collinear & not (o,p,a) are_collinear by A53, A111, Th1;

          then (b1,r,z) are_collinear by A115, A55, A107, A125, A131, Th14;

          then (z,r,b1) are_collinear by Th1;

          then (z,b1,b3) are_collinear by A114, A134, Th2;

          then (b1,b3,z) are_collinear by Th1;

          then (c1,c3,c2) are_collinear by A15, A16, A28, A30, A50, A51, A52, Th14;

          hence contradiction by A85, Th1;

        end;

        

         A135: not (p,o,a) are_collinear by A111, Th1;

        now

          (a3,a2,c1) are_collinear & (a3,a2,p) are_collinear by A13, A54, Th1;

          then (a3,c1,p) are_collinear by A29, Th2;

          then

           A136: (p,a3,c1) are_collinear by Th1;

          

           A137: (b1,c3,b2) are_collinear by A12, Th1;

          ( not (a1,o,a3) are_collinear ) & (a1,o,b1) are_collinear by A8, A17, Th1;

          then not (a1,b1,a3) are_collinear by A2, Th6;

          then

           A138: not (a1,a3,b1) are_collinear by Th1;

          assume

           A139: b1 = q;

          then

           A140: (b1,a3,a) are_collinear by A90, Th1;

          (c1,a,z) are_collinear by A52, A74, A34, Th2;

          then

           A141: (a,c1,z) are_collinear by Th1;

          (a2,b2,o) are_collinear by A18, Th1;

          then not (b1,o,b2) are_collinear by A1, A3, A7, A17, Th13;

          then

           A142: not (b1,b2,o) are_collinear by Th1;

          consider z9 be Element of PCPP such that

           A143: (b1,b3,z9) are_collinear & (p,o,z9) are_collinear by ANPROJ_2:def 14;

          (b1,c3,p) are_collinear by A67, A139, Th1;

          then

           A144: (b1,b2,p) are_collinear by A17, A33, A137, Th2;

          (o,b2,a) are_collinear by A18, A75, A47, Th2;

          then (c1,z9,a) are_collinear by A5, A6, A14, A19, A27, A73, A110, A143, A144, A142, A140, A136, Th16;

          then

           A145: (a,c1,z9) are_collinear by Th1;

          (p,o,z) are_collinear by A53, Th1;

          then (b1,b3,z) are_collinear by A55, A106, A135, A143, A145, A141, Th14;

          then (c1,c3,c2) are_collinear by A15, A16, A28, A50, A51, A52, A138, Th14;

          hence contradiction by A85, Th1;

        end;

        hence contradiction by A119;

      end;

      

       A146: b2 <> b3 by A3, A9, A18, A19, Th7;

      

       A147: b1 <> b2 by A1, A7, A17, A18, Th7;

      now

         A148:

        now

          assume

           A149: (b1,b2,b3) are_collinear ;

          then (b2,b3,b1) are_collinear by Th1;

          then (b2,b1,c1) are_collinear by A14, A146, Th2;

          then

           A150: (b1,b2,c1) are_collinear by Th1;

          (b1,b3,b2) are_collinear by A149, Th1;

          then (b1,b2,c2) are_collinear by A16, A24, Th2;

          hence thesis by A12, A147, A150, ANPROJ_2:def 8;

        end;

         A151:

        now

          assume

           A152: (a1,a2,a3) are_collinear ;

          then (a2,a3,a1) are_collinear by Th1;

          then (a2,a1,c1) are_collinear by A13, A29, Th2;

          then

           A153: (a1,a2,c1) are_collinear by Th1;

          (a1,a3,a2) are_collinear by A152, Th1;

          then (a1,a2,c2) are_collinear by A15, A28, Th2;

          hence thesis by A11, A25, A153, ANPROJ_2:def 8;

        end;

        assume (a1,a2,a3) are_collinear or (b1,b2,b3) are_collinear ;

        hence thesis by A151, A148;

      end;

      hence thesis by A31;

    end;

    

     Lm3: o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not (o,a1,a2) are_collinear & not (o,a1,a3) are_collinear & not (o,a2,a3) are_collinear & not (o,c1,c3) are_collinear & (a1,a2,c3) are_collinear & (b1,b2,c3) are_collinear & (a2,a3,c1) are_collinear & (b2,b3,c1) are_collinear & (a1,a3,c2) are_collinear & (b1,b3,c2) are_collinear & (o,a1,b1) are_collinear & (o,a2,b2) are_collinear & (o,a3,b3) are_collinear implies (c1,c2,c3) are_collinear

    proof

      assume that

       A1: o <> b1 and

       A2: a1 <> b1 and

       A3: o <> b2 and

       A4: a2 <> b2 and

       A5: o <> b3 and

       A6: a3 <> b3 and

       A7: not (o,a1,a2) are_collinear and

       A8: not (o,a1,a3) are_collinear and

       A9: not (o,a2,a3) are_collinear and

       A10: not (o,c1,c3) are_collinear and

       A11: (a1,a2,c3) are_collinear & (b1,b2,c3) are_collinear and

       A12: (a2,a3,c1) are_collinear and

       A13: (b2,b3,c1) are_collinear and

       A14: (a1,a3,c2) are_collinear & (b1,b3,c2) are_collinear and

       A15: (o,a1,b1) are_collinear and

       A16: (o,a2,b2) are_collinear and

       A17: (o,a3,b3) are_collinear ;

      

       A18: o <> a2 by A7, ANPROJ_2:def 7;

      

       A19: a1 <> a3 by A8, ANPROJ_2:def 7;

      

       A20: o <> a1 & o <> a3 by A8, ANPROJ_2:def 7;

      now

        assume that not (a1,a2,a3) are_collinear and not (b1,b2,b3) are_collinear ;

        consider x such that

         A21: (a1,a3,x) are_collinear and

         A22: (o,a2,x) are_collinear by ANPROJ_2:def 14;

        consider y such that

         A23: (b1,b3,y) are_collinear and

         A24: (o,a2,y) are_collinear by ANPROJ_2:def 14;

        assume

         A25: not thesis;

         A26:

        now

          ( not (o,a3,a2) are_collinear ) & (b3,b2,c1) are_collinear by A9, A13, Th1;

          then

           A27: a2 <> c1 by A4, A5, A16, A17, Th8;

           not (a2,a3,o) are_collinear by A9, Th1;

          then not (a2,c1,o) are_collinear by A12, A27, Th6;

          then

           A28: not (o,a2,c1) are_collinear by Th1;

          

           A29: b1 <> b3 by A1, A8, A15, A17, Th7;

          ( not (a1,o,a3) are_collinear ) & (a1,o,b1) are_collinear by A8, A15, Th1;

          then not (a1,b1,a3) are_collinear by A2, Th6;

          then

           A30: not (a1,a3,b1) are_collinear by Th1;

          assume that

           A31: (c1,c3,x) are_collinear and

           A32: (c1,c3,y) are_collinear ;

          c1 <> c3 & o <> a2 by A7, A10, ANPROJ_2:def 7;

          then (b1,b3,x) are_collinear by A22, A23, A24, A31, A32, A28, Th14;

          then (c1,c3,c2) are_collinear by A14, A19, A21, A31, A29, A30, Th14;

          hence contradiction by A25, Th1;

        end;

        now

           A33:

          now

            

             A34: not (o,b1,b3) are_collinear by A1, A5, A8, A15, A17, Th15;

            

             A35: (o,b2,a2) are_collinear & (o,b3,a3) are_collinear by A16, A17, Th1;

            

             A36: (o,b2,y) are_collinear & (o,b1,a1) are_collinear by A15, A16, A18, A24, Th1, Th2;

            assume

             A37: not (c1,c3,y) are_collinear ;

            ( not (o,b1,b2) are_collinear ) & not (o,b2,b3) are_collinear by A1, A3, A5, A7, A9, A15, A16, A17, Th15;

            hence contradiction by A2, A4, A6, A10, A11, A12, A13, A14, A18, A20, A23, A25, A37, A36, A35, A34, Lm2;

          end;

          assume not (c1,c3,x) are_collinear or not (c1,c3,y) are_collinear ;

          hence thesis by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A21, A22, A33, Lm2;

        end;

        hence thesis by A26;

      end;

      hence thesis by A1, A3, A7, A8, A9, A11, A12, A13, A14, A15, A16, A17, Lm1;

    end;

    theorem :: HESSENBE:17

    

     Th17: o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & not (o,a1,a2) are_collinear & not (o,a1,a3) are_collinear & not (o,a2,a3) are_collinear & (a1,a2,c3) are_collinear & (b1,b2,c3) are_collinear & (a2,a3,c1) are_collinear & (b2,b3,c1) are_collinear & (a1,a3,c2) are_collinear & (b1,b3,c2) are_collinear & (o,a1,b1) are_collinear & (o,a2,b2) are_collinear & (o,a3,b3) are_collinear implies (c1,c2,c3) are_collinear

    proof

      assume that

       A1: o <> b1 & a1 <> b1 & o <> b2 & a2 <> b2 & o <> b3 & a3 <> b3 & ( not (o,a1,a2) are_collinear ) & not (o,a1,a3) are_collinear and

       A2: not (o,a2,a3) are_collinear and

       A3: (a1,a2,c3) are_collinear & (b1,b2,c3) are_collinear and

       A4: (a2,a3,c1) are_collinear and

       A5: (b2,b3,c1) are_collinear and

       A6: (a1,a3,c2) are_collinear & (b1,b3,c2) are_collinear & (o,a1,b1) are_collinear & (o,a2,b2) are_collinear & (o,a3,b3) are_collinear ;

      

       A7: o <> c1 by A2, A4, Th1;

      

       A8: (b3,b2,c1) are_collinear by A5, Th1;

      

       A9: ( not (o,a3,a2) are_collinear ) & (a3,a2,c1) are_collinear by A2, A4, Th1;

      now

        assume (o,c1,c3) are_collinear ;

        then

         A10: (c1,c3,o) are_collinear by Th1;

        assume not thesis;

        then

         A11: not (c1,c3,c2) are_collinear by Th1;

        then not (c1,o,c2) are_collinear by A7, A10, Th6;

        then not (o,c1,c2) are_collinear by Th1;

        hence contradiction by A1, A3, A6, A9, A8, A11, Lm3;

      end;

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

    end;

    registration

      cluster Pappian -> Desarguesian for CollProjectiveSpace;

      coherence

      proof

        let PCPP be CollProjectiveSpace such that

         A1: PCPP is Pappian;

         A2:

        now

          assume not ex p,p1,q,q1 be Element of PCPP st not ex r be Element of PCPP st (p,p1,r) are_collinear & (q,q1,r) are_collinear ;

          then PCPP is Pappian CollProjectivePlane by A1, ANPROJ_2:def 14;

          then for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 be Element of PCPP st o <> q1 & p1 <> q1 & o <> q2 & p2 <> q2 & o <> q3 & p3 <> q3 & not (o,p1,p2) are_collinear & not (o,p1,p3) are_collinear & not (o,p2,p3) are_collinear & (p1,p2,r3) are_collinear & (q1,q2,r3) are_collinear & (p2,p3,r1) are_collinear & (q2,q3,r1) are_collinear & (p1,p3,r2) are_collinear & (q1,q3,r2) are_collinear & (o,p1,q1) are_collinear & (o,p2,q2) are_collinear & (o,p3,q3) are_collinear holds (r1,r2,r3) are_collinear by Th17;

          hence thesis by ANPROJ_2:def 12;

        end;

        now

          assume ex p,p1,q,q1 be Element of PCPP st not ex r be Element of PCPP st (p,p1,r) are_collinear & (q,q1,r) are_collinear ;

          then PCPP is up-3-dimensional CollProjectiveSpace by ANPROJ_2:def 14;

          hence thesis;

        end;

        hence thesis by A2;

      end;

    end