projdes1.miz



    begin

    reserve FCPS for up-3-dimensional CollProjectiveSpace;

    reserve a,a9,b,b9,c,c9,d,d9,o,p,q,r,s,t,u,x,y,z for Element of FCPS;

    theorem :: PROJDES1: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 :: PROJDES1:2

    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, COLLSP: 12;

      hence thesis;

    end;

    theorem :: PROJDES1:3

     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, COLLSP: 6;

    end;

    theorem :: PROJDES1:4

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

    

     Th5: not (o,a,d) are_collinear & (o,d,d9) are_collinear & d <> d9 & (a9,d9,s) are_collinear & (o,a,a9) are_collinear & o <> a9 implies s <> 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,s) 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, COLLSP: 6;

      then

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

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

      hence contradiction by A1, A6, A8, COLLSP: 6;

    end;

    

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

    proof

      assume that

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

       A2: (a,b,b9) are_collinear and

       A3: (a,c,c9) are_collinear and

       A4: a <> b9;

      assume not thesis;

      then

       A5: (a,b9,c) are_collinear by A3, Th1;

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

      hence contradiction by A1, A4, A5, COLLSP: 6;

    end;

    definition

      let FCPS, a, b, c, d;

      :: PROJDES1:def1

      pred a,b,c,d are_coplanar means ex x be Element of FCPS st (a,b,x) are_collinear & (c,d,x) are_collinear ;

    end

    theorem :: PROJDES1:6

    

     Th6: (a,b,c) are_collinear or (b,c,d) are_collinear or (c,d,a) are_collinear or (d,a,b) are_collinear implies (a,b,c,d) are_coplanar

    proof

       A1:

      now

        

         A2: (c,d,c) are_collinear by ANPROJ_2:def 7;

        assume (a,b,c) are_collinear ;

        hence thesis by A2;

      end;

       A3:

      now

        

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

        assume (c,d,a) are_collinear ;

        hence thesis by A4;

      end;

       A5:

      now

        assume (d,a,b) are_collinear ;

        then

         A6: (a,b,d) are_collinear by Th1;

        (c,d,d) are_collinear by ANPROJ_2:def 7;

        hence thesis by A6;

      end;

       A7:

      now

        assume (b,c,d) are_collinear ;

        then

         A8: (c,d,b) are_collinear by Th1;

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

        hence thesis by A8;

      end;

      assume (a,b,c) are_collinear or (b,c,d) are_collinear or (c,d,a) are_collinear or (d,a,b) are_collinear ;

      hence thesis by A1, A7, A3, A5;

    end;

    

     Lm2: (a,b,c,d) are_coplanar implies (b,a,c,d) are_coplanar

    proof

      assume (a,b,c,d) are_coplanar ;

      then

      consider x such that

       A1: (a,b,x) are_collinear and

       A2: (c,d,x) are_collinear ;

      (b,a,x) are_collinear by A1, Th1;

      hence thesis by A2;

    end;

    

     Lm3: (a,b,c,d) are_coplanar implies (b,c,d,a) are_coplanar

    proof

      assume (a,b,c,d) are_coplanar ;

      then

      consider x such that

       A1: (a,b,x) are_collinear & (c,d,x) are_collinear ;

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

      then

      consider y such that

       A2: (b,c,y) are_collinear and

       A3: (a,d,y) are_collinear by ANPROJ_2:def 9;

      (d,a,y) are_collinear by A3, Th1;

      hence thesis by A2;

    end;

    theorem :: PROJDES1:7

    

     Th7: (a,b,c,d) are_coplanar implies (b,c,d,a) are_coplanar & (c,d,a,b) are_coplanar & (d,a,b,c) are_coplanar & (b,a,c,d) are_coplanar & (c,b,d,a) are_coplanar & (d,c,a,b) are_coplanar & (a,d,b,c) are_coplanar & (a,c,d,b) are_coplanar & (b,d,a,c) are_coplanar & (c,a,b,d) are_coplanar & (d,b,c,a) are_coplanar & (c,a,d,b) are_coplanar & (d,b,a,c) are_coplanar & (a,c,b,d) are_coplanar & (b,d,c,a) are_coplanar & (a,b,d,c) are_coplanar & (a,d,c,b) are_coplanar & (b,c,a,d) are_coplanar & (b,a,d,c) are_coplanar & (c,b,a,d) are_coplanar & (c,d,b,a) are_coplanar & (d,a,c,b) are_coplanar & (d,c,b,a) are_coplanar

    proof

      assume

       A1: (a,b,c,d) are_coplanar ;

      then (b,a,c,d) are_coplanar by Lm2;

      then (a,c,d,b) are_coplanar by Lm3;

      then

       A2: (c,d,b,a) are_coplanar by Lm3;

      then

       A3: (d,b,a,c) are_coplanar by Lm3;

      then (b,d,a,c) are_coplanar by Lm2;

      then

       A4: (d,a,c,b) are_coplanar by Lm3;

      then (a,c,b,d) are_coplanar by Lm3;

      then (c,a,b,d) are_coplanar by Lm2;

      then

       A5: (a,b,d,c) are_coplanar by Lm3;

      then

       A6: (b,d,c,a) are_coplanar by Lm3;

      then (d,c,a,b) are_coplanar by Lm3;

      then (c,d,a,b) are_coplanar by Lm2;

      then

       A7: (d,a,b,c) are_coplanar by Lm3;

      then (a,d,b,c) are_coplanar by Lm2;

      then (d,b,c,a) are_coplanar by Lm3;

      then (b,c,a,d) are_coplanar by Lm3;

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

    end;

    

     Lm4: not (a,b,c) are_collinear & (a,b,c,p) are_coplanar & (a,b,c,q) are_coplanar implies (a,b,p,q) are_coplanar

    proof

      assume that

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

       A2: (a,b,c,p) are_coplanar and

       A3: (a,b,c,q) are_coplanar ;

      consider x such that

       A4: (a,b,x) are_collinear and

       A5: (c,p,x) are_collinear by A2;

      consider y such that

       A6: (a,b,y) are_collinear and

       A7: (c,q,y) are_collinear by A3;

       A8:

      now

        assume

         A9: a <> b;

        (b,a,x) are_collinear & (b,a,y) are_collinear by A4, A6, Th1;

        then (b,x,y) are_collinear by A9, COLLSP: 6;

        then

         A10: (x,y,b) are_collinear by Th1;

        (a,x,y) are_collinear by A4, A6, A9, COLLSP: 6;

        then

         A11: (x,y,a) are_collinear by Th1;

         A12:

        now

          (p,c,x) are_collinear by A5, Th1;

          then

          consider z such that

           A13: (p,q,z) are_collinear and

           A14: (x,y,z) are_collinear by A7, ANPROJ_2:def 9;

          assume x <> y;

          then (a,b,z) are_collinear by A11, A10, A14, ANPROJ_2:def 8;

          hence thesis by A13;

        end;

        now

          assume x = y;

          then

           A15: (x,c,q) are_collinear by A7, Th1;

          (x,c,p) are_collinear by A5, Th1;

          then (x,p,q) are_collinear by A1, A4, A15, COLLSP: 6;

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

          hence thesis by A4;

        end;

        hence thesis by A12;

      end;

      now

        assume a = b;

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

        hence thesis by Th6;

      end;

      hence thesis by A8;

    end;

    theorem :: PROJDES1:8

    

     Th8: not (a,b,c) are_collinear & (a,b,c,p) are_coplanar & (a,b,c,q) are_coplanar & (a,b,c,r) are_coplanar & (a,b,c,s) are_coplanar implies (p,q,r,s) are_coplanar

    proof

      assume that

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

       A2: (a,b,c,p) are_coplanar and

       A3: (a,b,c,q) are_coplanar and

       A4: (a,b,c,r) are_coplanar and

       A5: (a,b,c,s) are_coplanar ;

      

       A6: (a,b,p,q) are_coplanar by A1, A2, A3, Lm4;

      

       A7: (a,b,q,r) are_coplanar by A1, A3, A4, Lm4;

      

       A8: (a,b,p,r) are_coplanar by A1, A2, A4, Lm4;

      

       A9: (a,b,q,s) are_coplanar by A1, A3, A5, Lm4;

       A10:

      now

        

         A11: (q,a,b,r) are_coplanar by A7, Th7;

        assume

         A12: not (a,b,q) are_collinear ;

        then

         A13: not (q,a,b) are_collinear by Th1;

        

         A14: (q,a,b,p) are_coplanar by A6, Th7;

        then

         A15: (q,a,p,r) are_coplanar by A13, A11, Lm4;

        

         A16: (q,a,b,s) are_coplanar by A9, Th7;

        then

         A17: (q,a,p,s) are_coplanar by A13, A14, Lm4;

         A18:

        now

          assume not (q,a,p) are_collinear ;

          then

           A19: not (q,p,a) are_collinear by Th1;

          (q,p,a,r) are_coplanar & (q,p,a,s) are_coplanar by A15, A17, Th7;

          then (q,p,r,s) are_coplanar by A19, Lm4;

          hence thesis by Th7;

        end;

        

         A20: (q,a,r,s) are_coplanar by A13, A11, A16, Lm4;

         A21:

        now

          assume not (q,a,r) are_collinear ;

          then

           A22: not (q,r,a) are_collinear by Th1;

          (q,r,a,p) are_coplanar & (q,r,a,s) are_coplanar by A15, A20, Th7;

          then (q,r,p,s) are_coplanar by A22, Lm4;

          hence thesis by Th7;

        end;

        

         A23: q <> a by A12, ANPROJ_2:def 7;

        now

          assume (q,a,p) are_collinear & (q,a,r) are_collinear ;

          then (q,p,r) are_collinear by A23, COLLSP: 6;

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

          hence thesis by Th6;

        end;

        hence thesis by A18, A21;

      end;

      

       A24: (a,b,r,s) are_coplanar by A1, A4, A5, Lm4;

       A25:

      now

        

         A26: (r,a,b,q) are_coplanar by A7, Th7;

        assume

         A27: not (a,b,r) are_collinear ;

        then

         A28: not (r,a,b) are_collinear by Th1;

        

         A29: (r,a,b,p) are_coplanar by A8, Th7;

        then

         A30: (r,a,p,q) are_coplanar by A28, A26, Lm4;

        

         A31: (r,a,b,s) are_coplanar by A24, Th7;

        then

         A32: (r,a,p,s) are_coplanar by A28, A29, Lm4;

         A33:

        now

          assume not (r,a,p) are_collinear ;

          then

           A34: not (r,p,a) are_collinear by Th1;

          (r,p,a,q) are_coplanar & (r,p,a,s) are_coplanar by A30, A32, Th7;

          then (r,p,q,s) are_coplanar by A34, Lm4;

          hence thesis by Th7;

        end;

        

         A35: (r,a,q,s) are_coplanar by A28, A26, A31, Lm4;

         A36:

        now

          assume not (r,a,q) are_collinear ;

          then

           A37: not (r,q,a) are_collinear by Th1;

          (r,q,a,p) are_coplanar & (r,q,a,s) are_coplanar by A30, A35, Th7;

          then (r,q,p,s) are_coplanar by A37, Lm4;

          hence thesis by Th7;

        end;

        

         A38: r <> a by A27, ANPROJ_2:def 7;

        now

          assume (r,a,p) are_collinear & (r,a,q) are_collinear ;

          then (r,p,q) are_collinear by A38, COLLSP: 6;

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

          hence thesis by Th6;

        end;

        hence thesis by A33, A36;

      end;

      

       A39: (a,b,p,s) are_coplanar by A1, A2, A5, Lm4;

       A40:

      now

        

         A41: (p,a,b,r) are_coplanar by A8, Th7;

        assume

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

        then

         A43: not (p,a,b) are_collinear by Th1;

        

         A44: (p,a,b,q) are_coplanar by A6, Th7;

        then

         A45: (p,a,q,r) are_coplanar by A43, A41, Lm4;

        

         A46: (p,a,b,s) are_coplanar by A39, Th7;

        then

         A47: (p,a,q,s) are_coplanar by A43, A44, Lm4;

         A48:

        now

          assume not (p,a,q) are_collinear ;

          then

           A49: not (p,q,a) are_collinear by Th1;

          (p,q,a,r) are_coplanar & (p,q,a,s) are_coplanar by A45, A47, Th7;

          hence thesis by A49, Lm4;

        end;

        

         A50: (p,a,r,s) are_coplanar by A43, A41, A46, Lm4;

         A51:

        now

          assume not (p,a,r) are_collinear ;

          then

           A52: not (p,r,a) are_collinear by Th1;

          (p,r,a,q) are_coplanar & (p,r,a,s) are_coplanar by A45, A50, Th7;

          then (p,r,q,s) are_coplanar by A52, Lm4;

          hence thesis by Th7;

        end;

        

         A53: p <> a by A42, ANPROJ_2:def 7;

        now

          assume (p,a,q) are_collinear & (p,a,r) are_collinear ;

          then (p,q,r) are_collinear by A53, COLLSP: 6;

          hence thesis by Th6;

        end;

        hence thesis by A48, A51;

      end;

      

       A54: a <> b by A1, ANPROJ_2:def 7;

      now

        assume (a,b,p) are_collinear & (a,b,q) are_collinear & (a,b,r) are_collinear ;

        then (p,q,r) are_collinear by A54, ANPROJ_2:def 8;

        hence thesis by Th6;

      end;

      hence thesis by A40, A10, A25;

    end;

    

     Lm5: not (a,b,c) are_collinear & (a,b,c,p) are_coplanar & (a,b,c,q) are_coplanar & (a,b,c,r) are_coplanar implies (a,p,q,r) are_coplanar

    proof

      assume that

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

       A2: (a,b,c,p) are_coplanar and

       A3: (a,b,c,q) are_coplanar and

       A4: (a,b,c,r) are_coplanar ;

      now

         A5:

        now

          (a,b,r,q) are_coplanar by A1, A3, A4, Lm4;

          then

           A6: (a,r,b,q) are_coplanar by Th7;

          (a,b,r,p) are_coplanar by A1, A2, A4, Lm4;

          then

           A7: (a,r,b,p) are_coplanar by Th7;

          assume not (a,r,b) are_collinear ;

          then (a,r,p,q) are_coplanar by A7, A6, Lm4;

          hence thesis by Th7;

        end;

         A8:

        now

          (a,b,p,r) are_coplanar by A1, A2, A4, Lm4;

          then

           A9: (a,p,b,r) are_coplanar by Th7;

          (a,b,p,q) are_coplanar by A1, A2, A3, Lm4;

          then

           A10: (a,p,b,q) are_coplanar by Th7;

          assume not (a,p,b) are_collinear ;

          hence thesis by A10, A9, Lm4;

        end;

         A11:

        now

          (a,b,q,r) are_coplanar by A1, A3, A4, Lm4;

          then

           A12: (a,q,b,r) are_coplanar by Th7;

          (a,b,q,p) are_coplanar by A1, A2, A3, Lm4;

          then

           A13: (a,q,b,p) are_coplanar by Th7;

          assume not (a,q,b) are_collinear ;

          then (a,q,p,r) are_coplanar by A13, A12, Lm4;

          hence thesis by Th7;

        end;

        assume

         A14: not (p,q,r) are_collinear ;

        a <> b by A1, ANPROJ_2:def 7;

        then not (a,b,p) are_collinear or not (a,b,q) are_collinear or not (a,b,r) are_collinear by A14, ANPROJ_2:def 8;

        hence thesis by A8, A11, A5, Th1;

      end;

      hence thesis by Th6;

    end;

    theorem :: PROJDES1:9

     not (p,q,r) are_collinear & (a,b,c,p) are_coplanar & (a,b,c,r) are_coplanar & (a,b,c,q) are_coplanar & (p,q,r,s) are_coplanar implies (a,b,c,s) are_coplanar

    proof

      assume that

       A1: not (p,q,r) are_collinear and

       A2: (a,b,c,p) are_coplanar and

       A3: (a,b,c,r) are_coplanar and

       A4: (a,b,c,q) are_coplanar and

       A5: (p,q,r,s) are_coplanar ;

      now

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

        then

         A6: (b,a,c,b) are_coplanar by Th6;

        

         A7: (b,a,c,r) are_coplanar by A3, Th7;

        assume

         A8: not (a,b,c) are_collinear ;

        then

         A9: not (b,a,c) are_collinear by Th1;

        (a,p,q,r) are_coplanar by A2, A3, A4, A8, Lm5;

        then

         A10: (p,q,r,a) are_coplanar by Th7;

        

         A11: (c,a,b,r) are_coplanar by A3, Th7;

        

         A12: not (c,a,b) are_collinear by A8, Th1;

        (c,a,b,p) are_coplanar & (c,a,b,q) are_coplanar by A2, A4, Th7;

        then (c,p,q,r) are_coplanar by A12, A11, Lm5;

        then

         A13: (p,q,r,c) are_coplanar by Th7;

        (b,a,c,p) are_coplanar & (b,a,c,q) are_coplanar by A2, A4, Th7;

        then (p,q,r,b) are_coplanar by A9, A6, A7, Th8;

        hence thesis by A1, A5, A10, A13, Th8;

      end;

      hence thesis by Th6;

    end;

    

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

    proof

      assume that

       A1: p <> q & (p,q,r) are_collinear and

       A2: (a,b,p,q) are_coplanar ;

      consider x such that

       A3: (a,b,x) are_collinear and

       A4: (p,q,x) are_collinear by A2;

      (p,r,x) are_collinear by A1, A4, COLLSP: 6;

      hence thesis by A3;

    end;

    theorem :: PROJDES1:10

    

     Th10: p <> q & (p,q,r) are_collinear & (a,b,c,p) are_coplanar & (a,b,c,q) are_coplanar implies (a,b,c,r) are_coplanar

    proof

      assume that

       A1: p <> q and

       A2: (p,q,r) are_collinear and

       A3: (a,b,c,p) are_coplanar and

       A4: (a,b,c,q) are_coplanar ;

      

       A5: (q,p,r) are_collinear by A2, Th1;

      now

        assume

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

        then (a,b,p,q) are_coplanar by A3, A4, Lm4;

        then

         A7: (a,b,p,r) are_coplanar by A1, A2, Lm6;

         A8:

        now

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

          then

           A9: (a,b,p,b) are_coplanar by Th6;

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

          then

           A10: (a,b,p,a) are_coplanar by Th6;

          assume

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

          (a,b,p,c) are_coplanar by A3, Th7;

          hence thesis by A7, A11, A10, A9, Th8;

        end;

        (a,b,q,p) are_coplanar by A3, A4, A6, Lm4;

        then

         A12: (a,b,q,r) are_coplanar by A1, A5, Lm6;

         A13:

        now

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

          then

           A14: (a,b,q,b) are_coplanar by Th6;

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

          then

           A15: (a,b,q,a) are_coplanar by Th6;

          assume

           A16: not (a,b,q) are_collinear ;

          (a,b,q,c) are_coplanar by A4, Th7;

          hence thesis by A12, A16, A15, A14, Th8;

        end;

        now

          assume (a,b,p) are_collinear & (a,b,q) are_collinear ;

          then (a,b,r) are_collinear by A1, A2, COLLSP: 9;

          then (r,a,b) are_collinear by Th1;

          hence thesis by Th6;

        end;

        hence thesis by A8, A13;

      end;

      hence thesis by Th6;

    end;

    theorem :: PROJDES1:11

     not (a,b,c) are_collinear & (a,b,c,p) are_coplanar & (a,b,c,q) are_coplanar & (a,b,c,r) are_coplanar & (a,b,c,s) are_coplanar implies ex x st (p,q,x) are_collinear & (r,s,x) are_collinear

    proof

      assume not (a,b,c) are_collinear & (a,b,c,p) are_coplanar & (a,b,c,q) are_coplanar & (a,b,c,r) are_coplanar & (a,b,c,s) are_coplanar ;

      then (p,q,r,s) are_coplanar by Th8;

      hence thesis;

    end;

    theorem :: PROJDES1:12

    

     Th12: ex a, b, c, d st not (a,b,c,d) are_coplanar

    proof

      consider a, b, c, d such that

       A1: not (a,b,x) are_collinear or not (c,d,x) are_collinear by ANPROJ_2:def 14;

      take a, b, c, d;

      thus thesis by A1;

    end;

    theorem :: PROJDES1:13

    

     Th13: not (p,q,r) are_collinear implies ex s st not (p,q,r,s) are_coplanar

    proof

      assume

       A1: not (p,q,r) are_collinear ;

      consider a, b, c, d such that

       A2: not (a,b,c,d) are_coplanar by Th12;

      assume

       A3: not thesis;

      then

       A4: (p,q,r,c) are_coplanar & (p,q,r,d) are_coplanar ;

      (p,q,r,a) are_coplanar & (p,q,r,b) are_coplanar by A3;

      hence contradiction by A1, A2, A4, Th8;

    end;

    theorem :: PROJDES1:14

    

     Th14: a = b or a = c or b = c or a = d or b = d or d = c implies (a,b,c,d) are_coplanar

    proof

       A1:

      now

        assume a = b or a = c or b = c;

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

        hence thesis by Th6;

      end;

       A2:

      now

        assume a = d or b = d;

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

        hence thesis by Th6;

      end;

       A3:

      now

        assume d = c;

        then (b,c,d) are_collinear by ANPROJ_2:def 7;

        hence thesis by Th6;

      end;

      assume a = b or a = c or b = c or a = d or b = d or d = c;

      hence thesis by A1, A2, A3;

    end;

    theorem :: PROJDES1:15

    

     Th15: not (a,b,c,o) are_coplanar & (o,a,a9) are_collinear & a <> a9 implies not (a,b,c,a9) are_coplanar

    proof

      assume that

       A1: not (a,b,c,o) are_coplanar and

       A2: (o,a,a9) are_collinear and

       A3: a <> a9;

      assume

       A4: not thesis;

      

       A5: (a,b,c,a) are_coplanar by Th14;

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

      hence contradiction by A1, A3, A4, A5, Th10;

    end;

    theorem :: PROJDES1:16

    

     Th16: not (a,b,c) are_collinear & not (a9,b9,c9) are_collinear & (a,b,c,p) are_coplanar & (a,b,c,q) are_coplanar & (a,b,c,r) are_coplanar & (a9,b9,c9,p) are_coplanar & (a9,b9,c9,q) are_coplanar & (a9,b9,c9,r) are_coplanar & not (a,b,c,a9) are_coplanar implies (p,q,r) are_collinear

    proof

      assume that

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

       A2: not (a9,b9,c9) are_collinear and

       A3: (a,b,c,p) are_coplanar & (a,b,c,q) are_coplanar & (a,b,c,r) are_coplanar and

       A4: (a9,b9,c9,p) are_coplanar & (a9,b9,c9,q) are_coplanar & (a9,b9,c9,r) are_coplanar and

       A5: not (a,b,c,a9) are_coplanar ;

      (a,b,c,a) are_coplanar by Th14;

      then

       A6: (p,q,r,a) are_coplanar by A1, A3, Th8;

      (a9,b9,c9,a9) are_coplanar by Th14;

      then

       A7: (p,q,r,a9) are_coplanar by A2, A4, Th8;

      (a,b,c,c) are_coplanar by Th14;

      then

       A8: (p,q,r,c) are_coplanar by A1, A3, Th8;

      (a,b,c,b) are_coplanar by Th14;

      then

       A9: (p,q,r,b) are_coplanar by A1, A3, Th8;

      assume not thesis;

      hence contradiction by A5, A6, A9, A8, A7, Th8;

    end;

    theorem :: PROJDES1:17

    

     Th17: a <> a9 & (o,a,a9) are_collinear & not (a,b,c,o) are_coplanar & not (a9,b9,c9) are_collinear & (a,b,p) are_collinear & (a9,b9,p) are_collinear & (b,c,q) are_collinear & (b9,c9,q) are_collinear & (a,c,r) are_collinear & (a9,c9,r) are_collinear implies (p,q,r) are_collinear

    proof

      assume that

       A1: a <> a9 & (o,a,a9) are_collinear & not (a,b,c,o) are_coplanar and

       A2: not (a9,b9,c9) are_collinear and

       A3: (a,b,p) are_collinear and

       A4: (a9,b9,p) are_collinear and

       A5: (b,c,q) are_collinear & (b9,c9,q) are_collinear and

       A6: (a,c,r) are_collinear and

       A7: (a9,c9,r) are_collinear ;

      

       A8: (a,b,c,q) are_coplanar & (a9,b9,c9,q) are_coplanar by A5, Th6;

      (c9,r,a9) are_collinear by A7, Th1;

      then

       A9: (a9,b9,c9,r) are_coplanar by Th6;

      (p,a9,b9) are_collinear by A4, Th1;

      then

       A10: (a9,b9,c9,p) are_coplanar by Th6;

      (c,r,a) are_collinear by A6, Th1;

      then

       A11: (a,b,c,r) are_coplanar by Th6;

      (p,a,b) are_collinear by A3, Th1;

      then

       A12: (a,b,c,p) are_coplanar by Th6;

      ( not (a,b,c,a9) are_coplanar ) & not (a,b,c) are_collinear by A1, Th6, Th15;

      hence thesis by A2, A12, A11, A10, A8, A9, Th16;

    end;

    theorem :: PROJDES1:18

    

     Th18: not (a,b,c,d) are_coplanar & (a,b,c,o) are_coplanar & not (a,b,o) are_collinear implies not (a,b,d,o) are_coplanar

    proof

      assume that

       A1: not (a,b,c,d) are_coplanar and

       A2: (a,b,c,o) are_coplanar and

       A3: not (a,b,o) are_collinear ;

      assume not thesis;

      then

       A4: (a,b,o,d) are_coplanar by Th7;

      (a,b,o,c) are_coplanar by A2, Th7;

      hence contradiction by A1, A3, A4, Lm4;

    end;

    theorem :: PROJDES1:19

    

     Th19: not (a,b,c,o) are_coplanar & (o,a,a9) are_collinear & (o,b,b9) are_collinear & (o,c,c9) are_collinear & o <> a9 & o <> b9 & o <> c9 implies not (a9,b9,c9) are_collinear & not (a9,b9,c9,o) are_coplanar

    proof

      assume that

       A1: ( not (a,b,c,o) are_coplanar ) & (o,a,a9) are_collinear and

       A2: (o,b,b9) are_collinear and

       A3: (o,c,c9) are_collinear and

       A4: o <> a9 and

       A5: o <> b9 and

       A6: o <> c9;

      (a,o,a9) are_collinear & not (o,b,c,a) are_coplanar by A1, Th1, Th7;

      then not (o,b,c,a9) are_coplanar by A4, Th15;

      then

       A7: not (o,a9,b,c) are_coplanar by Th7;

      (c,o,c9) are_collinear by A3, Th1;

      then not (o,a9,b,c9) are_coplanar by A6, A7, Th15;

      then

       A8: not (o,a9,c9,b) are_coplanar by Th7;

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

      then not (o,a9,c9,b9) are_coplanar by A5, A8, Th15;

      then not (a9,b9,c9,o) are_coplanar by Th7;

      hence thesis by Th6;

    end;

    theorem :: PROJDES1:20

    

     Th20: (a,b,c,o) are_coplanar & not (a,b,c,d) are_coplanar & not (a,b,d,o) are_coplanar & (o,d,d9) are_collinear & (o,a,a9) are_collinear & (o,b,b9) are_collinear & (a,d,s) are_collinear & (a9,d9,s) are_collinear & (b,d,t) are_collinear & (b9,d9,t) are_collinear & (c,d,u) are_collinear & o <> a9 & d <> d9 & o <> b9 implies not (s,t,u) are_collinear

    proof

      assume that

       A1: (a,b,c,o) are_coplanar and

       A2: not (a,b,c,d) are_coplanar and

       A3: not (a,b,d,o) are_coplanar and

       A4: (o,d,d9) are_collinear and

       A5: (o,a,a9) are_collinear and

       A6: (o,b,b9) are_collinear and

       A7: (a,d,s) are_collinear and

       A8: (a9,d9,s) are_collinear and

       A9: (b,d,t) are_collinear and

       A10: (b9,d9,t) are_collinear and

       A11: (c,d,u) are_collinear and

       A12: o <> a9 and

       A13: d <> d9 and

       A14: o <> b9;

      

       A15: (d,b,c,b) are_coplanar by Th14;

      

       A16: not (d,b,c,a) are_coplanar by A2, Th7;

      then

       A17: not (d,b,c) are_collinear by Th6;

       not (b,d,o) are_collinear by A3, Th6;

      then not (o,b,d) are_collinear by Th1;

      then

       A18: t <> d by A4, A6, A10, A13, A14, Th5;

      (d,b,t) are_collinear & (d,c,u) are_collinear by A9, A11, Th1;

      then

       A19: t <> u by A17, A18, Lm1;

      

       A20: (d,b,c,d) are_coplanar by Th14;

       not (d,o,a) are_collinear by A3, Th6;

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

      then s <> d by A4, A5, A8, A12, A13, Th5;

      then

       A21: not (d,b,c,s) are_coplanar by A7, A16, Th15;

      b <> d by A2, Th14;

      then

       A22: (d,b,c,t) are_coplanar by A9, A15, A20, Th10;

      (d,b,c,c) are_coplanar by Th14;

      then (d,b,c,u) are_coplanar by A1, A3, A11, A20, Th10;

      then not (t,u,s) are_collinear by A21, A22, A19, Th10;

      hence thesis by Th1;

    end;

    definition

      let FCPS, o, a, b, c;

      :: PROJDES1:def2

      pred o,a,b,c constitute_a_quadrangle means not (a,b,c) are_collinear & not (o,a,b) are_collinear & not (o,b,c) are_collinear & not (o,c,a) are_collinear ;

    end

    

     Lm7: o <> a9 & o <> b9 & o <> c9 & a <> a9 & b <> b9 & (o,a,b,c) constitute_a_quadrangle & (o,a,a9) are_collinear & (o,b,b9) are_collinear & (o,c,c9) are_collinear & (a,b,p) are_collinear & (a9,b9,p) are_collinear & (b,c,q) are_collinear & (b9,c9,q) are_collinear & (a,c,r) are_collinear & (a9,c9,r) are_collinear implies (p,q,r) are_collinear

    proof

      assume that

       A1: o <> a9 and

       A2: o <> b9 and

       A3: o <> c9 and

       A4: a <> a9 and

       A5: b <> b9 and

       A6: (o,a,b,c) constitute_a_quadrangle and

       A7: (o,a,a9) are_collinear and

       A8: (o,b,b9) are_collinear and

       A9: (o,c,c9) are_collinear and

       A10: (a,b,p) are_collinear and

       A11: (a9,b9,p) are_collinear and

       A12: (b,c,q) are_collinear and

       A13: (b9,c9,q) are_collinear and

       A14: (a,c,r) are_collinear and

       A15: (a9,c9,r) are_collinear ;

      

       A16: not (o,b,c) are_collinear by A6;

      

       A17: not (a,b,c) are_collinear by A6;

      

       A18: not (o,c,a) are_collinear by A6;

      

       A19: not (o,a,b) are_collinear by A6;

       A20:

      now

        assume

         A21: (a,b,c,o) are_coplanar ;

        then

         A22: (b,c,a,o) are_coplanar by Th7;

        

         A23: (a,c,b,o) are_coplanar by A21, Th7;

        consider d such that

         A24: not (a,b,c,d) are_coplanar by A17, Th13;

        

         A25: not (a,c,b,d) are_coplanar by A24, Th7;

        

         A26: (a,b,c,c) are_coplanar by Th14;

        

         A27: not (b,c,a,d) are_coplanar by A24, Th7;

        consider d9 such that

         A28: o <> d9 and

         A29: d <> d9 and

         A30: (o,d,d9) are_collinear by ANPROJ_2:def 10;

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

        then

        consider s such that

         A31: (a,d,s) are_collinear and

         A32: (a9,d9,s) are_collinear by A30, ANPROJ_2:def 9;

        

         A33: (d,a,s) are_collinear by A31, Th1;

        (b,o,b9) are_collinear by A8, Th1;

        then

        consider t such that

         A34: (b,d,t) are_collinear & (b9,d9,t) are_collinear by A30, ANPROJ_2:def 9;

        (c,o,c9) are_collinear by A9, Th1;

        then

        consider u such that

         A35: (c,d,u) are_collinear and

         A36: (c9,d9,u) are_collinear by A30, ANPROJ_2:def 9;

        

         A37: (s,t,u,s) are_coplanar by Th14;

         not (a,c,o) are_collinear by A18, Th1;

        then

         A38: not (a,c,d,o) are_coplanar by A25, A23, Th18;

        then not (a9,c9,d9) are_collinear by A1, A3, A7, A9, A28, A30, Th19;

        then (r,u,s) are_collinear by A4, A7, A14, A15, A31, A32, A35, A36, A38, Th17;

        then

         A39: (s,u,r) are_collinear by Th1;

         not (a,b,o) are_collinear by A19, Th1;

        then

         A40: not (a,b,d,o) are_coplanar by A21, A24, Th18;

        then not (d,o,a) are_collinear by Th6;

        then

         A41: not (o,d,a) are_collinear by Th1;

        

         A42: (s,t,u,u) are_coplanar by Th14;

         not (b,c,o) are_collinear by A16, Th1;

        then

         A43: not (b,c,d,o) are_coplanar by A27, A22, Th18;

        then not (b9,c9,d9) are_collinear by A2, A3, A8, A9, A28, A30, Th19;

        then (q,u,t) are_collinear by A5, A8, A12, A13, A34, A35, A36, A43, Th17;

        then

         A44: (u,t,q) are_collinear by Th1;

        

         A45: (s,t,u,t) are_coplanar by Th14;

        (d9,a9,s) are_collinear by A32, Th1;

        then s <> a by A4, A7, A28, A30, A41, Th5;

        then

         A46: not (a,b,c,s) are_coplanar by A24, A33, Th15;

        

         A47: (a,b,c,b) are_coplanar by Th14;

         not (a9,b9,d9) are_collinear by A1, A2, A7, A8, A28, A30, A40, Th19;

        then (p,t,s) are_collinear by A4, A7, A10, A11, A31, A32, A34, A40, Th17;

        then

         A48: (t,s,p) are_collinear by Th1;

        

         A49: (a,b,c,a) are_coplanar by Th14;

        

         A50: not (s,t,u) are_collinear by A1, A2, A7, A8, A21, A24, A29, A30, A31, A32, A34, A35, A40, Th20;

        then t <> u by ANPROJ_2:def 7;

        then

         A51: (s,t,u,q) are_coplanar by A44, A45, A42, Th10;

        c <> a by A18, ANPROJ_2:def 7;

        then

         A52: (a,b,c,r) are_coplanar by A14, A49, A26, Th10;

        b <> c by A16, ANPROJ_2:def 7;

        then

         A53: (a,b,c,q) are_coplanar by A12, A47, A26, Th10;

        a <> b by A19, ANPROJ_2:def 7;

        then

         A54: (a,b,c,p) are_coplanar by A10, A49, A47, Th10;

        u <> s by A50, ANPROJ_2:def 7;

        then

         A55: (s,t,u,r) are_coplanar by A39, A37, A42, Th10;

        s <> t by A50, ANPROJ_2:def 7;

        then (s,t,u,p) are_coplanar by A48, A37, A45, Th10;

        hence thesis by A17, A50, A46, A54, A53, A52, A51, A55, Th16;

      end;

      now

        assume

         A56: not (a,b,c,o) are_coplanar ;

        then not (a9,b9,c9) are_collinear by A1, A2, A3, A7, A8, A9, Th19;

        hence thesis by A4, A7, A10, A11, A12, A13, A14, A15, A56, Th17;

      end;

      hence thesis by A20;

    end;

    theorem :: PROJDES1:21

    

     Th21: not (o,a,b) are_collinear & not (o,b,c) are_collinear & not (o,a,c) are_collinear & (o,a,a9) are_collinear & (o,b,b9) are_collinear & (o,c,c9) are_collinear & (a,b,p) are_collinear & (a9,b9,p) are_collinear & a <> a9 & (b,c,r) are_collinear & (b9,c9,r) are_collinear & (a,c,q) are_collinear & b <> b9 & (a9,c9,q) are_collinear & o <> a9 & o <> b9 & o <> c9 implies (r,q,p) are_collinear

    proof

      assume that

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

       A2: not (o,b,c) are_collinear and

       A3: not (o,a,c) are_collinear and

       A4: (o,a,a9) are_collinear & (o,b,b9) are_collinear & (o,c,c9) are_collinear and

       A5: (a,b,p) are_collinear and

       A6: (a9,b9,p) are_collinear & a <> a9 and

       A7: (b,c,r) are_collinear and

       A8: (b9,c9,r) are_collinear and

       A9: (a,c,q) are_collinear and

       A10: b <> b9 & (a9,c9,q) are_collinear & o <> a9 & o <> b9 & o <> c9;

       A11:

      now

        

         A12: b <> c & (b,c,b) are_collinear by A2, ANPROJ_2:def 7;

        assume

         A13: (a,b,c) are_collinear ;

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

        then

         A14: (a,b,r) are_collinear by A7, A12, ANPROJ_2:def 8;

        

         A15: c <> a & (a,c,a) are_collinear by A3, ANPROJ_2:def 7;

        (a,c,b) are_collinear by A13, Th1;

        then

         A16: (a,b,q) are_collinear by A9, A15, ANPROJ_2:def 8;

        a <> b by A1, ANPROJ_2:def 7;

        hence thesis by A5, A14, A16, ANPROJ_2:def 8;

      end;

      

       A17: not (o,c,a) are_collinear by A3, Th1;

      now

        assume not (a,b,c) are_collinear ;

        then (o,a,b,c) constitute_a_quadrangle by A1, A2, A17;

        then (p,r,q) are_collinear by A4, A5, A6, A7, A8, A9, A10, Lm7;

        hence thesis by Th1;

      end;

      hence thesis by A11;

    end;

    theorem :: PROJDES1:22

    

     Th22: for CS be up-3-dimensional CollProjectiveSpace holds CS is Desarguesian

    proof

      let CS be up-3-dimensional CollProjectiveSpace;

      for o,a,b,c,a9,b9,c9,r,q,p be Element of CS st o <> a9 & a <> a9 & o <> b9 & b <> b9 & o <> c9 & c <> c9 & not (o,a,b) are_collinear & not (o,a,c) are_collinear & not (o,b,c) are_collinear & (a,b,p) are_collinear & (a9,b9,p) are_collinear & (b,c,r) are_collinear & (b9,c9,r) are_collinear & (a,c,q) are_collinear & (a9,c9,q) are_collinear & (o,a,a9) are_collinear & (o,b,b9) are_collinear & (o,c,c9) are_collinear holds (r,q,p) are_collinear by Th21;

      hence thesis by ANPROJ_2:def 12;

    end;

    registration

      cluster -> Desarguesian for up-3-dimensional CollProjectiveSpace;

      correctness by Th22;

    end