aff_2.miz



    begin

    reserve AP for AffinPlane,

a,a9,b,b9,c,c9,x,y,o,p,q,r,s for Element of AP,

A,C,C9,D,K,M,N,P,T for Subset of AP;

    definition

      let AP;

      :: AFF_2:def1

      attr AP is satisfying_PPAP means for M, N, a, b, c, a9, b9, c9 st M is being_line & N is being_line & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & (a,b9) // (b,a9) & (b,c9) // (c,b9) holds (a,c9) // (c,a9);

    end

    definition

      let AP be AffinSpace;

      :: AFF_2:def2

      attr AP is Pappian means for M,N be Subset of AP, o,a,b,c,a9,b9,c9 be Element of AP st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & (a,b9) // (b,a9) & (b,c9) // (c,b9) holds (a,c9) // (c,a9);

    end

    definition

      let AP;

      :: AFF_2:def3

      attr AP is satisfying_PAP_1 means for M, N, o, a, b, c, a9, b9, c9 st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & b9 in N & c9 in N & (a,b9) // (b,a9) & (b,c9) // (c,b9) & (a,c9) // (c,a9) & b <> c holds a9 in N;

    end

    definition

      let AP be AffinSpace;

      :: AFF_2:def4

      attr AP is Desarguesian means for A,P,C be Subset of AP, o,a,b,c,a9,b9,c9 be Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & (a,b) // (a9,b9) & (a,c) // (a9,c9) holds (b,c) // (b9,c9);

    end

    definition

      let AP;

      :: AFF_2:def5

      attr AP is satisfying_DES_1 means for A, P, C, o, a, b, c, a9, b9, c9 st o in A & o in P & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & (a,b) // (a9,b9) & (a,c) // (a9,c9) & (b,c) // (b9,c9) & not LIN (a,b,c) & c <> c9 holds o in C;

    end

    definition

      let AP;

      :: AFF_2:def6

      attr AP is satisfying_DES_2 means for A, P, C, o, a, b, c, a9, b9, c9 st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & (a,b) // (a9,b9) & (a,c) // (a9,c9) & (b,c) // (b9,c9) holds c9 in C;

    end

    definition

      let AP be AffinSpace;

      :: AFF_2:def7

      attr AP is Moufangian means for K be Subset of AP, o,a,b,c,a9,b9,c9 be Element of AP st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN (o,a,a9) & LIN (o,b,b9) & (a,b) // (a9,b9) & (a,c) // (a9,c9) & (a,b) // K holds (b,c) // (b9,c9);

    end

    definition

      let AP;

      :: AFF_2:def8

      attr AP is satisfying_TDES_1 means for K, o, a, b, c, a9, b9, c9 st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN (o,a,a9) & (a,b) // (a9,b9) & (b,c) // (b9,c9) & (a,c) // (a9,c9) & (a,b) // K holds LIN (o,b,b9);

    end

    definition

      let AP;

      :: AFF_2:def9

      attr AP is satisfying_TDES_2 means for K, o, a, b, c, a9, b9, c9 st K is being_line & o in K & c in K & c9 in K & not a in K & o <> c & a <> b & LIN (o,a,a9) & LIN (o,b,b9) & (b,c) // (b9,c9) & (a,c) // (a9,c9) & (a,b) // K holds (a,b) // (a9,b9);

    end

    definition

      let AP;

      :: AFF_2:def10

      attr AP is satisfying_TDES_3 means for K, o, a, b, c, a9, b9, c9 st K is being_line & o in K & c in K & not a in K & o <> c & a <> b & LIN (o,a,a9) & LIN (o,b,b9) & (a,b) // (a9,b9) & (a,c) // (a9,c9) & (b,c) // (b9,c9) & (a,b) // K holds c9 in K;

    end

    definition

      let AP be AffinSpace;

      :: AFF_2:def11

      attr AP is translational means for A,P,C be Subset of AP, a,b,c,a9,b9,c9 be Element of AP st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & (a,b) // (a9,b9) & (a,c) // (a9,c9) holds (b,c) // (b9,c9);

    end

    definition

      let AP;

      :: AFF_2:def12

      attr AP is satisfying_des_1 means for A, P, C, a, b, c, a9, b9, c9 st A // P & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & (a,b) // (a9,b9) & (a,c) // (a9,c9) & (b,c) // (b9,c9) & not LIN (a,b,c) & c <> c9 holds A // C;

    end

    definition

      let AP be AffinSpace;

      :: AFF_2:def13

      attr AP is satisfying_pap means for M,N be Subset of AP, a,b,c,a9,b9,c9 be Element of AP st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & c9 in N & (a,b9) // (b,a9) & (b,c9) // (c,b9) holds (a,c9) // (c,a9);

    end

    definition

      let AP;

      :: AFF_2:def14

      attr AP is satisfying_pap_1 means for M, N, a, b, c, a9, b9, c9 st M is being_line & N is being_line & a in M & b in M & c in M & M // N & M <> N & a9 in N & b9 in N & (a,b9) // (b,a9) & (b,c9) // (c,b9) & (a,c9) // (c,a9) & a9 <> b9 holds c9 in N;

    end

    theorem :: AFF_2:1

    AP is Pappian iff AP is satisfying_PAP_1

    proof

      hereby

        assume

         A1: AP is Pappian;

        thus AP is satisfying_PAP_1

        proof

          let M, N, o, a, b, c, a9, b9, c9;

          assume that

           A2: M is being_line and

           A3: N is being_line and

           A4: M <> N and

           A5: o in M and

           A6: o in N and

           A7: o <> a and o <> a9 and

           A8: o <> b and

           A9: o <> b9 and

           A10: o <> c and

           A11: o <> c9 and

           A12: a in M and

           A13: b in M and

           A14: c in M and

           A15: b9 in N and

           A16: c9 in N and

           A17: (a,b9) // (b,a9) and

           A18: (b,c9) // (c,b9) and

           A19: (a,c9) // (c,a9) and

           A20: b <> c;

          

           A21: a <> c9 by A2, A3, A4, A5, A6, A7, A12, A16, AFF_1: 18;

          

           A22: b <> a9

          proof

            assume b = a9;

            then (c,b) // (a,c9) by A19, AFF_1: 4;

            then c9 in M by A2, A12, A13, A14, A20, AFF_1: 48;

            hence contradiction by A2, A3, A4, A5, A6, A11, A16, AFF_1: 18;

          end;

           not (b,a9) // N

          proof

            assume

             A23: (b,a9) // N;

            (b,a9) // (a,b9) by A17, AFF_1: 4;

            then (a,b9) // N by A22, A23, AFF_1: 32;

            then (b9,a) // N by AFF_1: 34;

            then a in N by A3, A15, AFF_1: 23;

            hence contradiction by A2, A3, A4, A5, A6, A7, A12, AFF_1: 18;

          end;

          then

          consider x such that

           A24: x in N and

           A25: LIN (b,a9,x) by A3, AFF_1: 59;

          

           A26: (b,a9) // (b,x) by A25, AFF_1:def 1;

          

           A27: o <> x

          proof

            assume o = x;

            then (b,o) // (a,b9) by A17, A22, A26, AFF_1: 5;

            then b9 in M by A2, A5, A8, A12, A13, AFF_1: 48;

            hence contradiction by A2, A3, A4, A5, A6, A9, A15, AFF_1: 18;

          end;

          (a,b9) // (b,x) by A17, A22, A26, AFF_1: 5;

          then (a,c9) // (c,x) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A18, A24, A27;

          then (c,a9) // (c,x) by A19, A21, AFF_1: 5;

          then LIN (c,a9,x) by AFF_1:def 1;

          then

           A28: LIN (a9,x,c) by AFF_1: 6;

          

           A29: LIN (a9,x,x) by AFF_1: 7;

          assume

           A30: not a9 in N;

           LIN (a9,x,b) by A25, AFF_1: 6;

          then x in M by A2, A13, A14, A20, A30, A24, A28, A29, AFF_1: 8, AFF_1: 25;

          hence contradiction by A2, A3, A4, A5, A6, A24, A27, AFF_1: 18;

        end;

      end;

      assume

       A31: AP is satisfying_PAP_1;

      let M, N, o, a, b, c, a9, b9, c9;

      assume that

       A32: M is being_line and

       A33: N is being_line and

       A34: M <> N & o in M & o in N and

       A35: o <> a and

       A36: o <> a9 and

       A37: o <> b and

       A38: o <> b9 and

       A39: o <> c & o <> c9 and

       A40: a in M and

       A41: b in M and

       A42: c in M and

       A43: a9 in N and

       A44: b9 in N and

       A45: c9 in N and

       A46: (a,b9) // (b,a9) and

       A47: (b,c9) // (c,b9);

      set A = ( Line (a,c9)), P = ( Line (b,a9));

      

       A48: b <> a9 by A32, A33, A34, A36, A41, A43, AFF_1: 18;

      then

       A49: b in P by AFF_1: 24;

      assume

       A50: not (a,c9) // (c,a9);

      then

       A51: a <> c9 by AFF_1: 3;

      then

       A52: a in A & c9 in A by AFF_1: 24;

      

       A53: a9 in P by A48, AFF_1: 24;

      A is being_line by A51, AFF_1: 24;

      then

      consider K such that

       A54: c in K and

       A55: A // K by AFF_1: 49;

      

       A56: b <> c

      proof

        assume

         A57: b = c;

        then LIN (b,c9,b9) by A47, AFF_1:def 1;

        then LIN (b9,c9,b) by AFF_1: 6;

        then b9 = c9 or b in N by A33, A44, A45, AFF_1: 25;

        hence contradiction by A32, A33, A34, A37, A41, A46, A50, A57, AFF_1: 18;

      end;

      

       A58: b9 <> c9

      proof

        assume b9 = c9;

        then (b9,b) // (b9,c) by A47, AFF_1: 4;

        then LIN (b9,b,c) by AFF_1:def 1;

        then LIN (b,c,b9) by AFF_1: 6;

        then b9 in M by A32, A41, A42, A56, AFF_1: 25;

        hence contradiction by A32, A33, A34, A38, A44, AFF_1: 18;

      end;

      

       A59: not P // K

      proof

        assume P // K;

        then P // A by A55, AFF_1: 44;

        then (b,a9) // (a,c9) by A52, A49, A53, AFF_1: 39;

        then (a,b9) // (a,c9) by A46, A48, AFF_1: 5;

        then LIN (a,b9,c9) by AFF_1:def 1;

        then LIN (b9,c9,a) by AFF_1: 6;

        then a in N by A33, A44, A45, A58, AFF_1: 25;

        hence contradiction by A32, A33, A34, A35, A40, AFF_1: 18;

      end;

      

       A60: P is being_line by A48, AFF_1: 24;

      K is being_line by A55, AFF_1: 36;

      then

      consider x such that

       A61: x in P and

       A62: x in K by A60, A59, AFF_1: 58;

      

       A63: (a,c9) // (c,x) by A52, A54, A55, A62, AFF_1: 39;

       LIN (b,x,a9) by A60, A49, A53, A61, AFF_1: 21;

      then (b,x) // (b,a9) by AFF_1:def 1;

      then (a,b9) // (b,x) by A46, A48, AFF_1: 5;

      then x in N by A31, A32, A33, A34, A35, A37, A38, A39, A40, A41, A42, A44, A45, A47, A56, A63;

      then N = P by A33, A43, A50, A60, A53, A61, A63, AFF_1: 18;

      hence contradiction by A32, A33, A34, A37, A41, A49, AFF_1: 18;

    end;

    theorem :: AFF_2:2

    AP is Desarguesian iff AP is satisfying_DES_1

    proof

      hereby

        assume

         A1: AP is Desarguesian;

        thus AP is satisfying_DES_1

        proof

          let A, P, C, o, a, b, c, a9, b9, c9;

          assume that

           A2: o in A and

           A3: o in P and

           A4: o <> a and

           A5: o <> b and o <> c and

           A6: a in A and

           A7: a9 in A and

           A8: b in P and

           A9: b9 in P and

           A10: c in C and

           A11: c9 in C and

           A12: A is being_line and

           A13: P is being_line and

           A14: C is being_line and

           A15: A <> P and

           A16: A <> C and

           A17: (a,b) // (a9,b9) and

           A18: (a,c) // (a9,c9) and

           A19: (b,c) // (b9,c9) and

           A20: not LIN (a,b,c) and

           A21: c <> c9;

          set K = ( Line (o,c9));

          assume

           A22: not o in C;

          then

           A23: K is being_line by A11, AFF_1: 24;

          

           A24: a9 <> c9

          proof

            assume

             A25: a9 = c9;

            then (b,c) // (a9,b9) by A19, AFF_1: 4;

            then (a,b) // (b,c) or a9 = b9 by A17, AFF_1: 5;

            then (b,a) // (b,c) or a9 = b9 by AFF_1: 4;

            then LIN (b,a,c) or a9 = b9 by AFF_1:def 1;

            hence contradiction by A2, A3, A7, A9, A11, A12, A13, A15, A20, A22, A25, AFF_1: 6, AFF_1: 18;

          end;

          

           A26: A <> K

          proof

            assume A = K;

            then

             A27: c9 in A by A2, AFF_1: 24;

            (a9,c9) // (a,c) by A18, AFF_1: 4;

            then c in A by A6, A7, A12, A24, A27, AFF_1: 48;

            hence contradiction by A10, A11, A12, A14, A16, A21, A27, AFF_1: 18;

          end;

          

           A28: a <> c by A20, AFF_1: 7;

          

           A29: o in K by A11, A22, AFF_1: 24;

          

           A30: c9 in K by A11, A22, AFF_1: 24;

           not (a,c) // K

          proof

            assume (a,c) // K;

            then (a9,c9) // K by A18, A28, AFF_1: 32;

            then (c9,a9) // K by AFF_1: 34;

            then a9 in K by A23, A30, AFF_1: 23;

            then

             A31: a9 in P by A2, A3, A7, A12, A23, A29, A26, AFF_1: 18;

            (a9,b9) // (b,a) by A17, AFF_1: 4;

            then a9 = b9 or a in P by A8, A9, A13, A31, AFF_1: 48;

            then (a,c) // (b,c) by A2, A3, A4, A6, A12, A13, A15, A18, A19, A24, AFF_1: 5, AFF_1: 18;

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

            then LIN (c,a,b) by AFF_1:def 1;

            hence contradiction by A20, AFF_1: 6;

          end;

          then

          consider x such that

           A32: x in K and

           A33: LIN (a,c,x) by A23, AFF_1: 59;

          

           A34: o <> x

          proof

            assume o = x;

            then LIN (a,o,c) by A33, AFF_1: 6;

            then

             A35: c in A by A2, A4, A6, A12, AFF_1: 25;

            then c9 in A by A6, A7, A12, A18, A28, AFF_1: 48;

            hence contradiction by A10, A11, A12, A14, A16, A21, A35, AFF_1: 18;

          end;

          

           A36: b9 <> c9

          proof

            assume b9 = c9;

            then a9 = b9 or (a,c) // (a,b) by A17, A18, AFF_1: 5;

            then a9 = b9 or LIN (a,c,b) by AFF_1:def 1;

            then (b,c) // (a,c) by A18, A19, A20, A24, AFF_1: 5, AFF_1: 6;

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

            then LIN (c,b,a) by AFF_1:def 1;

            hence contradiction by A20, AFF_1: 6;

          end;

          

           A37: (a,c) // (a,x) by A33, AFF_1:def 1;

          then (a,x) // (a9,c9) by A18, A28, AFF_1: 5;

          then (b,x) // (b9,c9) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A12, A13, A15, A17, A23, A29, A30, A26, A32, A34;

          then

           A38: (b,x) // (b,c) by A19, A36, AFF_1: 5;

          

           A39: not LIN (a,b,x)

          proof

            assume LIN (a,b,x);

            then (a,b) // (a,x) by AFF_1:def 1;

            then (a,b) // (a,c) or a = x by A37, AFF_1: 5;

            hence contradiction by A2, A4, A6, A12, A20, A23, A29, A26, A32, AFF_1: 18, AFF_1:def 1;

          end;

           LIN (a,x,c) by A33, AFF_1: 6;

          then c in K by A32, A39, A38, AFF_1: 14;

          hence contradiction by A10, A11, A14, A21, A22, A23, A29, A30, AFF_1: 18;

        end;

      end;

      assume

       A40: AP is satisfying_DES_1;

      let A, P, C, o, a, b, c, a9, b9, c9;

      assume that

       A41: o in A and

       A42: o in P and

       A43: o in C and

       A44: o <> a and

       A45: o <> b and

       A46: o <> c and

       A47: a in A and

       A48: a9 in A and

       A49: b in P and

       A50: b9 in P and

       A51: c in C and

       A52: c9 in C and

       A53: A is being_line and

       A54: P is being_line and

       A55: C is being_line and

       A56: A <> P and

       A57: A <> C and

       A58: (a,b) // (a9,b9) and

       A59: (a,c) // (a9,c9);

      assume

       A60: not (b,c) // (b9,c9);

      

       A61: a9 <> b9

      proof

        

         A62: (a9,c9) // (c,a) by A59, AFF_1: 4;

        assume

         A63: a9 = b9;

        then a9 in C by A41, A42, A43, A48, A50, A53, A54, A56, AFF_1: 18;

        then a in C or a9 = c9 by A51, A52, A55, A62, AFF_1: 48;

        hence contradiction by A41, A43, A44, A47, A53, A55, A57, A60, A63, AFF_1: 3, AFF_1: 18;

      end;

      

       A64: a9 <> c9

      proof

        assume a9 = c9;

        then

         A65: a9 in P by A41, A42, A43, A48, A52, A53, A55, A57, AFF_1: 18;

        (a9,b9) // (b,a) by A58, AFF_1: 4;

        then a in P by A49, A50, A54, A61, A65, AFF_1: 48;

        hence contradiction by A41, A42, A44, A47, A53, A54, A56, AFF_1: 18;

      end;

      

       A66: o <> c9

      proof

        assume

         A67: o = c9;

        (a9,c9) // (a,c) by A59, AFF_1: 4;

        then c in A by A41, A47, A48, A53, A64, A67, AFF_1: 48;

        hence contradiction by A41, A43, A46, A51, A53, A55, A57, AFF_1: 18;

      end;

      set M = ( Line (a,c)), N = ( Line (b9,c9));

      

       A68: a <> c by A41, A43, A44, A47, A51, A53, A55, A57, AFF_1: 18;

      then

       A69: c in M by AFF_1: 24;

      

       A70: a <> b by A41, A42, A44, A47, A49, A53, A54, A56, AFF_1: 18;

      

       A71: not LIN (a9,b9,c9)

      proof

        assume

         A72: LIN (a9,b9,c9);

        then (a9,b9) // (a9,c9) by AFF_1:def 1;

        then (a9,b9) // (a,c) by A59, A64, AFF_1: 5;

        then (a,b) // (a,c) by A58, A61, AFF_1: 5;

        then LIN (a,b,c) by AFF_1:def 1;

        then LIN (b,c,a) by AFF_1: 6;

        then (b,c) // (b,a) by AFF_1:def 1;

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

        then

         A73: (b,c) // (a9,b9) by A58, A70, AFF_1: 5;

         LIN (b9,c9,a9) by A72, AFF_1: 6;

        then (b9,c9) // (b9,a9) by AFF_1:def 1;

        then (b9,c9) // (a9,b9) by AFF_1: 4;

        hence contradiction by A60, A61, A73, AFF_1: 5;

      end;

      

       A74: b9 <> c9 by A60, AFF_1: 3;

      then

       A75: b9 in N & c9 in N by AFF_1: 24;

      N is being_line by A74, AFF_1: 24;

      then

      consider D such that

       A76: b in D and

       A77: N // D by AFF_1: 49;

      

       A78: a in M by A68, AFF_1: 24;

      

       A79: not M // D

      proof

        assume M // D;

        then M // N by A77, AFF_1: 44;

        then (a,c) // (b9,c9) by A78, A69, A75, AFF_1: 39;

        then (a9,c9) // (b9,c9) by A59, A68, AFF_1: 5;

        then (c9,a9) // (c9,b9) by AFF_1: 4;

        then LIN (c9,a9,b9) by AFF_1:def 1;

        hence contradiction by A71, AFF_1: 6;

      end;

      

       A80: M is being_line by A68, AFF_1: 24;

      D is being_line by A77, AFF_1: 36;

      then

      consider x such that

       A81: x in M and

       A82: x in D by A80, A79, AFF_1: 58;

       LIN (a,c,x) by A80, A78, A69, A81, AFF_1: 21;

      then (a,c) // (a,x) by AFF_1:def 1;

      then

       A83: (a,x) // (a9,c9) by A59, A68, AFF_1: 5;

      set T = ( Line (c9,x));

      

       A84: a <> a9

      proof

        assume

         A85: a = a9;

        then LIN (a,c,c9) by A59, AFF_1:def 1;

        then LIN (c,c9,a) by AFF_1: 6;

        then

         A86: c = c9 or a in C by A51, A52, A55, AFF_1: 25;

         LIN (a,b,b9) by A58, A85, AFF_1:def 1;

        then LIN (b,b9,a) by AFF_1: 6;

        then b = b9 or a in P by A49, A50, A54, AFF_1: 25;

        hence contradiction by A41, A42, A43, A44, A47, A53, A54, A55, A56, A57, A60, A86, AFF_1: 2, AFF_1: 18;

      end;

      

       A87: x <> c9

      proof

        assume x = c9;

        then (c9,a) // (c9,a9) by A83, AFF_1: 4;

        then LIN (c9,a,a9) by AFF_1:def 1;

        then LIN (a,a9,c9) by AFF_1: 6;

        then c9 in A by A47, A48, A53, A84, AFF_1: 25;

        hence contradiction by A41, A43, A52, A53, A55, A57, A66, AFF_1: 18;

      end;

      then

       A88: T is being_line & c9 in T by AFF_1: 24;

      

       A89: (b,x) // (b9,c9) by A75, A76, A77, A82, AFF_1: 39;

      

       A90: x in T by A87, AFF_1: 24;

      

       A91: a <> x

      proof

        assume a = x;

        then (a,b) // (b9,c9) by A75, A76, A77, A82, AFF_1: 39;

        then (a9,b9) // (b9,c9) by A58, A70, AFF_1: 5;

        then (b9,a9) // (b9,c9) by AFF_1: 4;

        then LIN (b9,a9,c9) by AFF_1:def 1;

        hence contradiction by A71, AFF_1: 6;

      end;

       not LIN (a,b,x)

      proof

        assume LIN (a,b,x);

        then (a,b) // (a,x) by AFF_1:def 1;

        then (a,b) // (a9,c9) by A83, A91, AFF_1: 5;

        then (a9,b9) // (a9,c9) by A58, A70, AFF_1: 5;

        hence contradiction by A71, AFF_1:def 1;

      end;

      then o in T by A40, A41, A42, A44, A45, A47, A48, A49, A50, A53, A54, A56, A58, A83, A89, A87, A88, A90;

      then x in C by A43, A52, A55, A66, A88, A90, AFF_1: 18;

      then C = M by A51, A55, A60, A80, A69, A81, A89, AFF_1: 18;

      hence contradiction by A41, A43, A44, A47, A53, A55, A57, A78, AFF_1: 18;

    end;

    theorem :: AFF_2:3

    

     Th3: AP is Moufangian implies AP is satisfying_TDES_1

    proof

      assume

       A1: AP is Moufangian;

      let K, o, a, b, c, a9, b9, c9;

      assume that

       A2: K is being_line and

       A3: o in K and

       A4: c in K and

       A5: c9 in K and

       A6: not a in K and

       A7: o <> c and

       A8: a <> b and

       A9: LIN (o,a,a9) and

       A10: (a,b) // (a9,b9) and

       A11: (b,c) // (b9,c9) and

       A12: (a,c) // (a9,c9) and

       A13: (a,b) // K;

      consider P such that

       A14: a9 in P and

       A15: K // P by A2, AFF_1: 49;

      

       A16: P is being_line by A15, AFF_1: 36;

      set A = ( Line (o,b)), C = ( Line (o,a));

      

       A17: o in A & b in A by AFF_1: 15;

      assume

       A18: not LIN (o,b,b9);

      then o <> b by AFF_1: 7;

      then

       A19: A is being_line by AFF_1:def 3;

      

       A20: not b in K by A6, A13, AFF_1: 35;

       not A // P

      proof

        assume A // P;

        then A // K by A15, AFF_1: 44;

        hence contradiction by A3, A20, A17, AFF_1: 45;

      end;

      then

      consider x such that

       A21: x in A and

       A22: x in P by A19, A16, AFF_1: 58;

      

       A23: o in C & a in C by AFF_1: 15;

      

       A24: LIN (o,b,x) by A19, A17, A21, AFF_1: 21;

      (a,b) // P by A13, A15, AFF_1: 43;

      then (a9,b9) // P by A8, A10, AFF_1: 32;

      then

       A25: b9 in P by A14, A16, AFF_1: 23;

      then

       A26: LIN (b9,x,b9) by A16, A22, AFF_1: 21;

      

       A27: C is being_line by A3, A6, AFF_1:def 3;

      then

       A28: a9 in C by A3, A6, A9, A23, AFF_1: 25;

      

       A29: b9 <> c9

      proof

        

         A30: (a9,c9) // (c,a) by A12, AFF_1: 4;

        assume

         A31: b9 = c9;

        then P = K by A5, A15, A25, AFF_1: 45;

        then a9 = o by A2, A3, A6, A27, A23, A28, A14, AFF_1: 18;

        then b9 = o by A2, A3, A4, A5, A6, A31, A30, AFF_1: 48;

        hence contradiction by A18, AFF_1: 7;

      end;

      

       A32: b <> c by A4, A6, A13, AFF_1: 35;

      (a9,x) // K by A14, A15, A22, AFF_1: 40;

      then (a,b) // (a9,x) by A2, A13, AFF_1: 31;

      then (b,c) // (x,c9) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A12, A13, A24;

      then (b9,c9) // (x,c9) by A11, A32, AFF_1: 5;

      then (c9,b9) // (c9,x) by AFF_1: 4;

      then LIN (c9,b9,x) by AFF_1:def 1;

      then

       A33: LIN (b9,x,c9) by AFF_1: 6;

      

       A34: a9 <> b9

      proof

        assume

         A35: a9 = b9;

         A36:

        now

          assume a9 = c9;

          then b9 = o by A2, A3, A5, A6, A27, A23, A28, A35, AFF_1: 18;

          hence contradiction by A18, AFF_1: 7;

        end;

        (a,c) // (b,c) or a9 = c9 by A11, A12, A35, AFF_1: 5;

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

        then LIN (c,a,b) by AFF_1:def 1;

        then LIN (a,c,b) by AFF_1: 6;

        then (a,c) // (a,b) by AFF_1:def 1;

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

        then (a,c) // K by A8, A13, AFF_1: 32;

        then (c,a) // K by AFF_1: 34;

        hence contradiction by A2, A4, A6, AFF_1: 23;

      end;

       LIN (b9,x,a9) by A14, A16, A22, A25, AFF_1: 21;

      then LIN (b9,c9,a9) by A18, A24, A33, A26, AFF_1: 8;

      then (b9,c9) // (b9,a9) by AFF_1:def 1;

      then (b9,c9) // (a9,b9) by AFF_1: 4;

      then (b,c) // (a9,b9) by A11, A29, AFF_1: 5;

      then (a,b) // (b,c) by A10, A34, AFF_1: 5;

      then (b,c) // K by A8, A13, AFF_1: 32;

      then (c,b) // K by AFF_1: 34;

      hence contradiction by A2, A4, A20, AFF_1: 23;

    end;

    theorem :: AFF_2:4

    AP is satisfying_TDES_1 implies AP is satisfying_TDES_2

    proof

      assume

       A1: AP is satisfying_TDES_1;

      let K, o, a, b, c, a9, b9, c9;

      assume that

       A2: K is being_line and

       A3: o in K and

       A4: c in K and

       A5: c9 in K and

       A6: not a in K and

       A7: o <> c and

       A8: a <> b and

       A9: LIN (o,a,a9) and

       A10: LIN (o,b,b9) and

       A11: (b,c) // (b9,c9) and

       A12: (a,c) // (a9,c9) and

       A13: (a,b) // K;

      set A = ( Line (o,a)), P = ( Line (o,b));

      

       A14: A is being_line & a in A by A3, A6, AFF_1: 24;

      

       A15: o in A by A3, A6, AFF_1: 24;

      then

       A16: a9 in A by A3, A6, A9, A14, AFF_1: 25;

      

       A17: o <> b by A3, A6, A13, AFF_1: 35;

      then

       A18: P is being_line by AFF_1: 24;

      consider N such that

       A19: a9 in N and

       A20: K // N by A2, AFF_1: 49;

      

       A21: N is being_line by A20, AFF_1: 36;

      set T = ( Line (b9,c9));

      

       A22: not b in K by A6, A13, AFF_1: 35;

      

       A23: b in P by A17, AFF_1: 24;

      

       A24: o in P by A17, AFF_1: 24;

      then

       A25: b9 in P by A10, A17, A18, A23, AFF_1: 25;

      assume

       A26: not (a,b) // (a9,b9);

      then

       A27: a9 <> b9 by AFF_1: 3;

      

       A28: not b9 in K

      proof

        

         A29: (a9,c9) // (a,c) by A12, AFF_1: 4;

        

         A30: (b9,c9) // (c,b) by A11, AFF_1: 4;

        assume

         A31: b9 in K;

        then b9 = o by A2, A3, A22, A18, A24, A23, A25, AFF_1: 18;

        then c9 in A by A2, A3, A4, A5, A22, A15, A30, AFF_1: 48;

        then a9 = c9 or c in A by A14, A16, A29, AFF_1: 48;

        hence contradiction by A2, A3, A4, A5, A6, A7, A27, A22, A15, A14, A31, A30, AFF_1: 18, AFF_1: 48;

      end;

      then

       A32: T is being_line by A5, AFF_1: 24;

      

       A33: b9 in T by A5, A28, AFF_1: 24;

      

       A34: c9 in T by A5, A28, AFF_1: 24;

       not N // T

      proof

        assume N // T;

        then K // T by A20, AFF_1: 44;

        hence contradiction by A5, A28, A33, A34, AFF_1: 45;

      end;

      then

      consider x such that

       A35: x in N and

       A36: x in T by A32, A21, AFF_1: 58;

      (a9,x) // K by A19, A20, A35, AFF_1: 40;

      then

       A37: (a,b) // (a9,x) by A2, A13, AFF_1: 31;

       LIN (c9,b9,x) by A32, A33, A34, A36, AFF_1: 21;

      then (c9,b9) // (c9,x) by AFF_1:def 1;

      then (b9,c9) // (x,c9) by AFF_1: 4;

      then (b,c) // (x,c9) by A5, A11, A28, AFF_1: 5;

      then LIN (o,b,x) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A12, A13, A37;

      then x in P by A17, A18, A24, A23, AFF_1: 25;

      then P = T by A26, A18, A25, A32, A33, A36, A37, AFF_1: 18;

      then LIN (c9,b9,b) by A18, A23, A33, A34, AFF_1: 21;

      then (c9,b9) // (c9,b) by AFF_1:def 1;

      then (b9,c9) // (b,c9) by AFF_1: 4;

      then (b,c) // (b,c9) by A5, A11, A28, AFF_1: 5;

      then LIN (b,c,c9) by AFF_1:def 1;

      then

       A38: LIN (c,c9,b) by AFF_1: 6;

      then (a,c) // (a9,c) by A2, A4, A5, A12, A22, AFF_1: 25;

      then (c,a) // (c,a9) by AFF_1: 4;

      then LIN (c,a,a9) by AFF_1:def 1;

      then LIN (a,a9,c) by AFF_1: 6;

      then

       A39: a = a9 or c in A by A14, A16, AFF_1: 25;

      (b,c) // (b9,c) by A2, A4, A5, A11, A22, A38, AFF_1: 25;

      then (c,b) // (c,b9) by AFF_1: 4;

      then LIN (c,b,b9) by AFF_1:def 1;

      then LIN (b,b9,c) by AFF_1: 6;

      then b = b9 or c in P by A18, A23, A25, AFF_1: 25;

      hence contradiction by A2, A3, A4, A6, A7, A26, A22, A18, A15, A14, A24, A23, A39, AFF_1: 2, AFF_1: 18;

    end;

    theorem :: AFF_2:5

    AP is satisfying_TDES_2 implies AP is satisfying_TDES_3

    proof

      assume

       A1: AP is satisfying_TDES_2;

      let K, o, a, b, c, a9, b9, c9;

      assume that

       A2: K is being_line and

       A3: o in K and

       A4: c in K and

       A5: not a in K and

       A6: o <> c and

       A7: a <> b and

       A8: LIN (o,a,a9) and

       A9: LIN (o,b,b9) and

       A10: (a,b) // (a9,b9) and

       A11: (a,c) // (a9,c9) and

       A12: (b,c) // (b9,c9) and

       A13: (a,b) // K;

      set A = ( Line (o,a)), P = ( Line (o,b)), N = ( Line (b,c));

      

       A14: o in A by A3, A5, AFF_1: 24;

      

       A15: not LIN (a,b,c)

      proof

        assume LIN (a,b,c);

        then (a,b) // (a,c) by AFF_1:def 1;

        then (a,c) // K by A7, A13, AFF_1: 32;

        then (c,a) // K by AFF_1: 34;

        hence contradiction by A2, A4, A5, AFF_1: 23;

      end;

      

       A16: o <> b by A3, A5, A13, AFF_1: 35;

      then

       A17: b in P by AFF_1: 24;

      

       A18: (a9,b9) // (b,a) by A10, AFF_1: 4;

      

       A19: b <> c by A4, A5, A13, AFF_1: 35;

      then

       A20: b in N & c in N by AFF_1: 24;

      

       A21: a in A by A3, A5, AFF_1: 24;

      

       A22: A is being_line by A3, A5, AFF_1: 24;

      

       A23: A <> P

      proof

        assume A = P;

        then (a,b) // A by A22, A21, A17, AFF_1: 40, AFF_1: 41;

        hence contradiction by A3, A5, A7, A13, A14, A21, AFF_1: 45, AFF_1: 53;

      end;

      assume

       A24: not c9 in K;

      

       A25: P is being_line by A16, AFF_1: 24;

      

       A26: o in P by A16, AFF_1: 24;

      then

       A27: b9 in P by A9, A16, A25, A17, AFF_1: 25;

      

       A28: a9 in A by A3, A5, A8, A22, A14, A21, AFF_1: 25;

      

       A29: a9 <> b9

      proof

        assume

         A30: a9 = b9;

        then (a,c) // (b,c) or a9 = c9 by A11, A12, AFF_1: 5;

        then (c,a) // (c,b) or a9 = c9 by AFF_1: 4;

        then LIN (c,a,b) or a9 = c9 by AFF_1:def 1;

        hence contradiction by A3, A24, A15, A22, A25, A14, A26, A28, A27, A23, A30, AFF_1: 6, AFF_1: 18;

      end;

      

       A31: a9 <> c9

      proof

        assume a9 = c9;

        then (b,c) // (a9,b9) by A12, AFF_1: 4;

        then (a,b) // (b,c) by A10, A29, AFF_1: 5;

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

        then LIN (b,a,c) by AFF_1:def 1;

        hence contradiction by A15, AFF_1: 6;

      end;

       not (a9,c9) // K

      proof

        assume

         A32: (a9,c9) // K;

        (a9,c9) // (a,c) by A11, AFF_1: 4;

        then (a,c) // K by A31, A32, AFF_1: 32;

        then (c,a) // K by AFF_1: 34;

        hence contradiction by A2, A4, A5, AFF_1: 23;

      end;

      then

      consider x such that

       A33: x in K and

       A34: LIN (a9,c9,x) by A2, AFF_1: 59;

      (a9,c9) // (a9,x) by A34, AFF_1:def 1;

      then

       A35: (a,c) // (a9,x) by A11, A31, AFF_1: 5;

      N is being_line by A19, AFF_1: 24;

      then

      consider T such that

       A36: x in T and

       A37: N // T by AFF_1: 49;

      

       A38: not b in K by A5, A13, AFF_1: 35;

      

       A39: not T // P

      proof

        assume T // P;

        then N // P by A37, AFF_1: 44;

        then c in P by A17, A20, AFF_1: 45;

        hence contradiction by A2, A3, A4, A6, A38, A25, A26, A17, AFF_1: 18;

      end;

      T is being_line by A37, AFF_1: 36;

      then

      consider y such that

       A40: y in T and

       A41: y in P by A25, A39, AFF_1: 58;

      

       A42: (b,c) // (y,x) by A20, A36, A37, A40, AFF_1: 39;

       A43:

      now

        assume y = b9;

        then (b9,c9) // (b9,x) by A12, A19, A42, AFF_1: 5;

        then LIN (b9,c9,x) by AFF_1:def 1;

        then

         A44: LIN (c9,x,b9) by AFF_1: 6;

         LIN (c9,x,a9) & LIN (c9,x,c9) by A34, AFF_1: 6, AFF_1: 7;

        then LIN (a9,b9,c9) by A24, A33, A44, AFF_1: 8;

        then (a9,b9) // (a9,c9) by AFF_1:def 1;

        then (a9,b9) // (a,c) by A11, A31, AFF_1: 5;

        then (a,b) // (a,c) by A10, A29, AFF_1: 5;

        hence contradiction by A15, AFF_1:def 1;

      end;

       LIN (o,b,y) by A25, A26, A17, A41, AFF_1: 21;

      then (a,b) // (a9,y) by A1, A2, A3, A4, A5, A6, A7, A8, A13, A33, A42, A35;

      then (a9,b9) // (a9,y) by A7, A10, AFF_1: 5;

      then LIN (a9,b9,y) by AFF_1:def 1;

      then LIN (b9,y,a9) by AFF_1: 6;

      then a9 in P by A25, A27, A41, A43, AFF_1: 25;

      then a in P by A25, A17, A27, A29, A18, AFF_1: 48;

      hence contradiction by A3, A5, A25, A26, A23, AFF_1: 24;

    end;

    theorem :: AFF_2:6

    AP is satisfying_TDES_3 implies AP is Moufangian

    proof

      assume

       A1: AP is satisfying_TDES_3;

      let K, o, a, b, c, a9, b9, c9;

      assume that

       A2: K is being_line and

       A3: o in K and

       A4: c in K and

       A5: c9 in K and

       A6: not a in K and

       A7: o <> c and

       A8: a <> b and

       A9: LIN (o,a,a9) and

       A10: LIN (o,b,b9) and

       A11: (a,b) // (a9,b9) and

       A12: (a,c) // (a9,c9) and

       A13: (a,b) // K;

      set A = ( Line (o,a)), P = ( Line (o,b)), M = ( Line (b,c)), T = ( Line (a9,c9));

      

       A14: o in A by A3, A6, AFF_1: 24;

      assume

       A15: not (b,c) // (b9,c9);

      then

       A16: b <> c by AFF_1: 3;

      then

       A17: b in M by AFF_1: 24;

      

       A18: (a9,b9) // (b,a) by A11, AFF_1: 4;

      

       A19: c in M by A16, AFF_1: 24;

      

       A20: a in A by A3, A6, AFF_1: 24;

      

       A21: A is being_line by A3, A6, AFF_1: 24;

      then

       A22: a9 in A by A3, A6, A9, A14, A20, AFF_1: 25;

      

       A23: o <> b by A3, A6, A13, AFF_1: 35;

      then

       A24: P is being_line by AFF_1: 24;

      

       A25: b in P by A23, AFF_1: 24;

      

       A26: A <> P

      proof

        assume A = P;

        then (a,b) // A by A21, A20, A25, AFF_1: 40, AFF_1: 41;

        hence contradiction by A3, A6, A8, A13, A14, A20, AFF_1: 45, AFF_1: 53;

      end;

      

       A27: o in P by A23, AFF_1: 24;

      then

       A28: b9 in P by A10, A23, A24, A25, AFF_1: 25;

      

       A29: a9 <> b9

      proof

        

         A30: (a9,c9) // (c,a) by A12, AFF_1: 4;

        assume

         A31: a9 = b9;

        then a9 in K by A3, A21, A24, A14, A27, A22, A28, A26, AFF_1: 18;

        then a9 = c9 by A2, A4, A5, A6, A30, AFF_1: 48;

        hence contradiction by A15, A31, AFF_1: 3;

      end;

      

       A32: a9 <> c9

      proof

        assume a9 = c9;

        then

         A33: a9 in P by A2, A3, A5, A6, A21, A14, A20, A27, A22, AFF_1: 18;

        (a9,b9) // (b,a) by A11, AFF_1: 4;

        then a in P by A24, A25, A28, A29, A33, AFF_1: 48;

        hence contradiction by A3, A6, A24, A27, A26, AFF_1: 24;

      end;

      then

       A34: T is being_line & c9 in T by AFF_1: 24;

      

       A35: M is being_line by A16, AFF_1: 24;

      then

      consider N such that

       A36: b9 in N and

       A37: M // N by AFF_1: 49;

      

       A38: N is being_line by A37, AFF_1: 36;

      

       A39: not LIN (a,b,c)

      proof

        assume LIN (a,b,c);

        then (a,b) // (a,c) by AFF_1:def 1;

        then (a,c) // K by A8, A13, AFF_1: 32;

        then (c,a) // K by AFF_1: 34;

        hence contradiction by A2, A4, A6, AFF_1: 23;

      end;

       not (a9,c9) // N

      proof

        assume

         A40: (a9,c9) // N;

        (a9,c9) // (a,c) by A12, AFF_1: 4;

        then (a,c) // N by A32, A40, AFF_1: 32;

        then (a,c) // M by A37, AFF_1: 43;

        then (c,a) // M by AFF_1: 34;

        then a in M by A35, A19, AFF_1: 23;

        hence contradiction by A39, A35, A17, A19, AFF_1: 21;

      end;

      then

      consider x such that

       A41: x in N and

       A42: LIN (a9,c9,x) by A38, AFF_1: 59;

      

       A43: (b,c) // (b9,x) by A17, A19, A36, A37, A41, AFF_1: 39;

      (a9,c9) // (a9,x) by A42, AFF_1:def 1;

      then (a,c) // (a9,x) by A12, A32, AFF_1: 5;

      then

       A44: x in K by A1, A2, A3, A4, A6, A7, A8, A9, A10, A11, A13, A43;

      

       A45: a9 in T by A32, AFF_1: 24;

      then x in T by A32, A34, A42, AFF_1: 25;

      then K = T by A2, A5, A15, A34, A43, A44, AFF_1: 18;

      then a9 in P by A2, A3, A6, A21, A14, A20, A27, A22, A45, AFF_1: 18;

      then a in P by A24, A25, A28, A29, A18, AFF_1: 48;

      hence contradiction by A3, A6, A24, A27, A26, AFF_1: 24;

    end;

    theorem :: AFF_2:7

    

     Th7: AP is translational iff AP is satisfying_des_1

    proof

      hereby

        assume

         A1: AP is translational;

        thus AP is satisfying_des_1

        proof

          let A, P, C, a, b, c, a9, b9, c9;

          assume that

           A2: A // P and

           A3: a in A and

           A4: a9 in A and

           A5: b in P and

           A6: b9 in P and

           A7: c in C & c9 in C and

           A8: A is being_line and

           A9: P is being_line and

           A10: C is being_line and

           A11: A <> P and

           A12: A <> C and

           A13: (a,b) // (a9,b9) and

           A14: (a,c) // (a9,c9) and

           A15: (b,c) // (b9,c9) and

           A16: not LIN (a,b,c) and

           A17: c <> c9;

          assume

           A18: not A // C;

          consider K such that

           A19: c9 in K and

           A20: A // K by A8, AFF_1: 49;

          

           A21: a <> c by A16, AFF_1: 7;

          

           A22: not (a,c) // K

          proof

            assume (a,c) // K;

            then (a,c) // A by A20, AFF_1: 43;

            then

             A23: c in A by A3, A8, AFF_1: 23;

            (a9,c9) // (a,c) by A14, AFF_1: 4;

            then (a9,c9) // A by A3, A8, A21, A23, AFF_1: 27;

            then c9 in A by A4, A8, AFF_1: 23;

            hence contradiction by A7, A8, A10, A12, A17, A23, AFF_1: 18;

          end;

          

           A24: A <> K

          proof

            assume

             A25: A = K;

            (a9,c9) // (a,c) by A14, AFF_1: 4;

            then a9 = c9 by A4, A19, A20, A22, A25, AFF_1: 32, AFF_1: 40;

            then (a9,b9) // (b,c) by A15, AFF_1: 4;

            then a9 = b9 or (a,b) // (b,c) by A13, AFF_1: 5;

            then b9 in A or (b,a) // (b,c) by A4, AFF_1: 4;

            then LIN (b,a,c) by A2, A6, A11, AFF_1: 45, AFF_1:def 1;

            hence contradiction by A16, AFF_1: 6;

          end;

           A26:

          now

            assume b9 = c9;

            then (a,b) // (a,c) or a9 = b9 by A13, A14, AFF_1: 5;

            hence contradiction by A2, A4, A6, A11, A16, AFF_1: 45, AFF_1:def 1;

          end;

          

           A27: K is being_line by A20, AFF_1: 36;

          then

          consider x such that

           A28: x in K and

           A29: LIN (a,c,x) by A22, AFF_1: 59;

          (a,c) // (a,x) by A29, AFF_1:def 1;

          then (a,x) // (a9,c9) by A14, A21, AFF_1: 5;

          then (b,x) // (b9,c9) by A1, A2, A3, A4, A5, A6, A8, A9, A11, A13, A19, A20, A27, A28, A24;

          then (b,x) // (b,c) or b9 = c9 by A15, AFF_1: 5;

          then LIN (b,x,c) by A26, AFF_1:def 1;

          then

           A30: LIN (x,c,b) by AFF_1: 6;

          

           A31: LIN (x,c,c) by AFF_1: 7;

           LIN (x,c,a) by A29, AFF_1: 6;

          then c in K by A16, A28, A30, A31, AFF_1: 8;

          hence contradiction by A7, A10, A17, A18, A19, A20, A27, AFF_1: 18;

        end;

      end;

      assume

       A32: AP is satisfying_des_1;

      let A, P, C, a, b, c, a9, b9, c9;

      assume that

       A33: A // P and

       A34: A // C and

       A35: a in A and

       A36: a9 in A and

       A37: b in P and

       A38: b9 in P and

       A39: c in C and

       A40: c9 in C and

       A41: A is being_line and

       A42: P is being_line and

       A43: C is being_line and

       A44: A <> P and

       A45: A <> C and

       A46: (a,b) // (a9,b9) and

       A47: (a,c) // (a9,c9);

      

       A48: a <> b by A33, A35, A37, A44, AFF_1: 45;

      

       A49: a9 <> b9 by A33, A36, A38, A44, AFF_1: 45;

      set K = ( Line (a,c)), N = ( Line (b9,c9));

      

       A50: a <> c by A34, A35, A39, A45, AFF_1: 45;

      then

       A51: a in K by AFF_1: 24;

      assume

       A52: not (b,c) // (b9,c9);

      then

       A53: b9 <> c9 by AFF_1: 3;

      then

       A54: b9 in N by AFF_1: 24;

      

       A55: b <> c by A52, AFF_1: 3;

      

       A56: not LIN (a,b,c)

      proof

        assume

         A57: LIN (a,b,c);

        then LIN (b,c,a) by AFF_1: 6;

        then (b,c) // (b,a) by AFF_1:def 1;

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

        then

         A58: (b,c) // (a9,b9) by A46, A48, AFF_1: 5;

         LIN (c,b,a) by A57, AFF_1: 6;

        then (c,b) // (c,a) by AFF_1:def 1;

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

        then (b,c) // (a9,c9) by A47, A50, AFF_1: 5;

        then (a9,c9) // (a9,b9) by A55, A58, AFF_1: 5;

        then LIN (a9,c9,b9) by AFF_1:def 1;

        then LIN (b9,c9,a9) by AFF_1: 6;

        then (b9,c9) // (b9,a9) by AFF_1:def 1;

        then (b9,c9) // (a9,b9) by AFF_1: 4;

        hence contradiction by A52, A49, A58, AFF_1: 5;

      end;

      

       A59: c in K by A50, AFF_1: 24;

      

       A60: N is being_line by A53, AFF_1: 24;

      then

      consider M such that

       A61: b in M and

       A62: N // M by AFF_1: 49;

      

       A63: c9 in N by A53, AFF_1: 24;

      

       A64: a9 <> c9 by A34, A36, A40, A45, AFF_1: 45;

      

       A65: not LIN (a9,b9,c9)

      proof

        assume LIN (a9,b9,c9);

        then (a9,b9) // (a9,c9) by AFF_1:def 1;

        then (a,b) // (a9,c9) by A46, A49, AFF_1: 5;

        then (a,b) // (a,c) by A47, A64, AFF_1: 5;

        hence contradiction by A56, AFF_1:def 1;

      end;

      

       A66: not K // M

      proof

        assume K // M;

        then K // N by A62, AFF_1: 44;

        then (a,c) // (b9,c9) by A51, A59, A54, A63, AFF_1: 39;

        then (a9,c9) // (b9,c9) by A47, A50, AFF_1: 5;

        then (c9,a9) // (c9,b9) by AFF_1: 4;

        then LIN (c9,a9,b9) by AFF_1:def 1;

        hence contradiction by A65, AFF_1: 6;

      end;

      

       A67: K is being_line by A50, AFF_1: 24;

      

       A68: M is being_line by A62, AFF_1: 36;

      then

      consider x such that

       A69: x in K and

       A70: x in M by A67, A66, AFF_1: 58;

      

       A71: (b,x) // (b9,c9) by A54, A63, A61, A62, A70, AFF_1: 39;

      set D = ( Line (x,c9));

      

       A72: A <> D

      proof

        assume A = D;

        then c9 in A by AFF_1: 15;

        hence contradiction by A34, A40, A45, AFF_1: 45;

      end;

      

       A73: x in D by AFF_1: 15;

       LIN (a,c,x) by A67, A51, A59, A69, AFF_1: 21;

      then (a,c) // (a,x) by AFF_1:def 1;

      then

       A74: (a,x) // (a9,c9) by A47, A50, AFF_1: 5;

      

       A75: c9 in D by AFF_1: 15;

      

       A76: not LIN (a,b,x)

      proof

        

         A77: a <> x

        proof

          assume a = x;

          then (a,b) // (b9,c9) by A54, A63, A61, A62, A70, AFF_1: 39;

          then (a9,b9) // (b9,c9) by A46, A48, AFF_1: 5;

          then (b9,a9) // (b9,c9) by AFF_1: 4;

          then LIN (b9,a9,c9) by AFF_1:def 1;

          hence contradiction by A65, AFF_1: 6;

        end;

        assume LIN (a,b,x);

        then LIN (x,b,a) by AFF_1: 6;

        then

         A78: (x,b) // (x,a) by AFF_1:def 1;

        x <> b by A67, A51, A59, A56, A69, AFF_1: 21;

        hence contradiction by A67, A51, A61, A68, A66, A69, A70, A78, A77, AFF_1: 38;

      end;

      

       A79: P // C by A33, A34, AFF_1: 44;

      

       A80: x <> c9

      proof

         A81:

        now

          

           A82: P // P by A33, AFF_1: 44;

          assume

           A83: P = N;

          then c in P by A39, A40, A79, A63, AFF_1: 45;

          hence contradiction by A37, A38, A52, A63, A83, A82, AFF_1: 39;

        end;

        assume x = c9;

        then M = N by A63, A62, A70, AFF_1: 45;

        then

         A84: P = N or b = b9 by A37, A38, A42, A60, A54, A61, AFF_1: 18;

        then (b,a) // (b,a9) by A46, A81, AFF_1: 4;

        then LIN (b,a,a9) by AFF_1:def 1;

        then LIN (a,a9,b) by AFF_1: 6;

        then b in A or a = a9 by A35, A36, A41, AFF_1: 25;

        then LIN (a9,c,c9) by A33, A37, A44, A47, AFF_1: 45, AFF_1:def 1;

        then LIN (c,c9,a9) by AFF_1: 6;

        then c = c9 or a9 in C by A39, A40, A43, AFF_1: 25;

        hence contradiction by A34, A36, A45, A52, A84, A81, AFF_1: 2, AFF_1: 45;

      end;

      then D is being_line by AFF_1: 24;

      then A // D by A32, A33, A35, A36, A37, A38, A41, A42, A44, A46, A71, A74, A73, A75, A80, A76, A72;

      then D // C by A34, AFF_1: 44;

      then C = D by A40, A75, AFF_1: 45;

      then C = K by A39, A43, A52, A67, A59, A69, A71, A73, AFF_1: 18;

      hence contradiction by A34, A35, A45, A51, AFF_1: 45;

    end;

    theorem :: AFF_2:8

    AP is satisfying_pap iff AP is satisfying_pap_1

    proof

      hereby

        assume

         A1: AP is satisfying_pap;

        thus AP is satisfying_pap_1

        proof

          let M, N, a, b, c, a9, b9, c9;

          assume that

           A2: M is being_line and

           A3: N is being_line and

           A4: a in M and

           A5: b in M and

           A6: c in M and

           A7: M // N and

           A8: M <> N and

           A9: a9 in N and

           A10: b9 in N and

           A11: (a,b9) // (b,a9) and

           A12: (b,c9) // (c,b9) and

           A13: (a,c9) // (c,a9) and

           A14: a9 <> b9;

          

           A15: c <> a9 by A6, A7, A8, A9, AFF_1: 45;

          set C = ( Line (c,b9));

          

           A16: c <> b9 by A6, A7, A8, A10, AFF_1: 45;

          then C is being_line by AFF_1: 24;

          then

          consider K such that

           A17: b in K and

           A18: C // K by AFF_1: 49;

          

           A19: c in C & b9 in C by A16, AFF_1: 24;

          

           A20: not K // N

          proof

            assume K // N;

            then C // N by A18, AFF_1: 44;

            then C // M by A7, AFF_1: 44;

            then b9 in M by A6, A19, AFF_1: 45;

            hence contradiction by A7, A8, A10, AFF_1: 45;

          end;

          K is being_line by A18, AFF_1: 36;

          then

          consider x such that

           A21: x in K and

           A22: x in N by A3, A20, AFF_1: 58;

          

           A23: (b,x) // (c,b9) by A19, A17, A18, A21, AFF_1: 39;

          then (a,x) // (c,a9) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A22;

          then (a,x) // (a,c9) by A13, A15, AFF_1: 5;

          then LIN (a,x,c9) by AFF_1:def 1;

          then

           A24: LIN (c9,x,a) by AFF_1: 6;

          

           A25: a <> b

          proof

            assume a = b;

            then LIN (a,b9,a9) by A11, AFF_1:def 1;

            then LIN (a9,b9,a) by AFF_1: 6;

            then a9 = b9 or a in N by A3, A9, A10, AFF_1: 25;

            hence contradiction by A4, A7, A8, A14, AFF_1: 45;

          end;

          

           A26: c9 <> b

          proof

            assume c9 = b;

            then a9 in M by A2, A4, A5, A6, A13, A25, AFF_1: 48;

            hence contradiction by A7, A8, A9, AFF_1: 45;

          end;

          (b,x) // (b,c9) by A12, A16, A23, AFF_1: 5;

          then LIN (b,x,c9) by AFF_1:def 1;

          then

           A27: LIN (c9,x,b) by AFF_1: 6;

          assume

           A28: not c9 in N;

           LIN (c9,x,c9) by AFF_1: 7;

          then c9 in M by A2, A4, A5, A28, A25, A22, A24, A27, AFF_1: 8, AFF_1: 25;

          then b9 in M by A2, A5, A6, A12, A26, AFF_1: 48;

          hence contradiction by A7, A8, A10, AFF_1: 45;

        end;

      end;

      assume

       A29: AP is satisfying_pap_1;

      let M, N, a, b, c, a9, b9, c9;

      assume that

       A30: M is being_line and

       A31: N is being_line and

       A32: a in M and

       A33: b in M and

       A34: c in M and

       A35: M // N & M <> N and

       A36: a9 in N and

       A37: b9 in N and

       A38: c9 in N and

       A39: (a,b9) // (b,a9) and

       A40: (b,c9) // (c,b9);

      set A = ( Line (c,a9)), D = ( Line (b,c9));

      

       A41: b <> c9 by A33, A35, A38, AFF_1: 45;

      then

       A42: b in D & c9 in D by AFF_1: 24;

      assume

       A43: not (a,c9) // (c,a9);

      then

       A44: c <> a9 by AFF_1: 3;

      then

       A45: c in A by AFF_1: 24;

      

       A46: a9 in A by A44, AFF_1: 24;

      

       A47: A is being_line by A44, AFF_1: 24;

      then

      consider P such that

       A48: a in P and

       A49: A // P by AFF_1: 49;

      

       A50: a9 <> b9

      proof

        assume

         A51: a9 = b9;

        then (a9,a) // (a9,b) by A39, AFF_1: 4;

        then LIN (a9,a,b) by AFF_1:def 1;

        then LIN (a,b,a9) by AFF_1: 6;

        then a = b or a9 in M by A30, A32, A33, AFF_1: 25;

        hence contradiction by A35, A36, A40, A43, A51, AFF_1: 45;

      end;

      

       A52: not D // P

      proof

        assume D // P;

        then (c,b9) // P by A40, A41, A42, AFF_1: 32, AFF_1: 40;

        then (c,b9) // A by A49, AFF_1: 43;

        then b9 in A by A47, A45, AFF_1: 23;

        then c in N by A31, A36, A37, A50, A47, A45, A46, AFF_1: 18;

        hence contradiction by A34, A35, AFF_1: 45;

      end;

      

       A53: D is being_line by A41, AFF_1: 24;

      P is being_line by A49, AFF_1: 36;

      then

      consider x such that

       A54: x in D and

       A55: x in P by A53, A52, AFF_1: 58;

       LIN (b,x,c9) by A53, A42, A54, AFF_1: 21;

      then (b,x) // (b,c9) by AFF_1:def 1;

      then

       A56: (b,x) // (c,b9) by A40, A41, AFF_1: 5;

      (a,x) // (c,a9) by A45, A46, A48, A49, A55, AFF_1: 39;

      then x in N by A29, A30, A31, A32, A33, A34, A35, A36, A37, A39, A50, A56;

      then x = c9 or b in N by A31, A38, A53, A42, A54, AFF_1: 18;

      hence contradiction by A33, A35, A43, A45, A46, A48, A49, A55, AFF_1: 39, AFF_1: 45;

    end;

    theorem :: AFF_2:9

    

     Th9: AP is Pappian implies AP is satisfying_pap

    proof

      assume

       A1: AP is Pappian;

      let M, N, a, b, c, a9, b9, c9;

      assume that

       A2: M is being_line and

       A3: N is being_line and

       A4: a in M and

       A5: b in M and

       A6: c in M and

       A7: M // N and

       A8: M <> N and

       A9: a9 in N and

       A10: b9 in N and

       A11: c9 in N and

       A12: (a,b9) // (b,a9) and

       A13: (b,c9) // (c,b9);

      

       A14: b <> a9 by A5, A7, A8, A9, AFF_1: 45;

      set K = ( Line (a,c9)), C = ( Line (c,b9));

      

       A15: c <> b9 by A6, A7, A8, A10, AFF_1: 45;

      then

       A16: C is being_line by AFF_1: 24;

      assume

       A17: not (a,c9) // (c,a9);

       A18:

      now

        assume

         A19: a = b;

        then LIN (a,b9,a9) by A12, AFF_1:def 1;

        then LIN (a9,b9,a) by AFF_1: 6;

        then a9 = b9 or a in N by A3, A9, A10, AFF_1: 25;

        hence contradiction by A4, A7, A8, A13, A17, A19, AFF_1: 45;

      end;

       A20:

      now

        assume a9 = b9;

        then (a9,a) // (a9,b) by A12, AFF_1: 4;

        then LIN (a9,a,b) by AFF_1:def 1;

        then LIN (a,b,a9) by AFF_1: 6;

        then a9 in M by A2, A4, A5, A18, AFF_1: 25;

        hence contradiction by A7, A8, A9, AFF_1: 45;

      end;

       A21:

      now

        assume

         A22: b = c;

        then LIN (b,c9,b9) by A13, AFF_1:def 1;

        then LIN (b9,c9,b) by AFF_1: 6;

        then b9 = c9 or b in N by A3, A10, A11, AFF_1: 25;

        hence contradiction by A5, A7, A8, A12, A17, A22, AFF_1: 45;

      end;

       A23:

      now

        assume b9 = c9;

        then (b9,b) // (b9,c) by A13, AFF_1: 4;

        then LIN (b9,b,c) by AFF_1:def 1;

        then LIN (b,c,b9) by AFF_1: 6;

        then b9 in M by A2, A5, A6, A21, AFF_1: 25;

        hence contradiction by A7, A8, A10, AFF_1: 45;

      end;

      

       A24: a <> c9 by A4, A7, A8, A11, AFF_1: 45;

      then

       A25: a in K by AFF_1: 24;

      K is being_line by A24, AFF_1: 24;

      then

      consider T such that

       A26: a9 in T and

       A27: K // T by AFF_1: 49;

      

       A28: T is being_line by A27, AFF_1: 36;

      

       A29: c9 in K by A24, AFF_1: 24;

      

       A30: c in C & b9 in C by A15, AFF_1: 24;

       not C // T

      proof

        assume C // T;

        then C // K by A27, AFF_1: 44;

        then (c,b9) // (a,c9) by A25, A29, A30, AFF_1: 39;

        then (b,c9) // (a,c9) by A13, A15, AFF_1: 5;

        then (c9,b) // (c9,a) by AFF_1: 4;

        then LIN (c9,b,a) by AFF_1:def 1;

        then LIN (a,b,c9) by AFF_1: 6;

        then c9 in M by A2, A4, A5, A18, AFF_1: 25;

        hence contradiction by A7, A8, A11, AFF_1: 45;

      end;

      then

      consider x such that

       A31: x in C and

       A32: x in T by A16, A28, AFF_1: 58;

      set D = ( Line (x,b));

      

       A33: x <> b

      proof

        assume x = b;

        then LIN (b,c,b9) by A16, A30, A31, AFF_1: 21;

        then b9 in M by A2, A5, A6, A21, AFF_1: 25;

        hence contradiction by A7, A8, A10, AFF_1: 45;

      end;

      then

       A34: b in D by AFF_1: 24;

      then

       A35: D <> N by A5, A7, A8, AFF_1: 45;

      

       A36: D is being_line by A33, AFF_1: 24;

      

       A37: x in D by A33, AFF_1: 24;

       not D // N

      proof

        assume D // N;

        then D // M by A7, AFF_1: 44;

        then x in M by A5, A37, A34, AFF_1: 45;

        then c in T or b9 in M by A2, A6, A16, A30, A31, A32, AFF_1: 18;

        hence contradiction by A7, A8, A10, A17, A25, A29, A26, A27, AFF_1: 39, AFF_1: 45;

      end;

      then

      consider o such that

       A38: o in D and

       A39: o in N by A3, A36, AFF_1: 58;

       LIN (b9,c,x) by A16, A30, A31, AFF_1: 21;

      then

       A40: (b9,c) // (b9,x) by AFF_1:def 1;

      

       A41: a9 <> x

      proof

        assume a9 = x;

        then (b9,a9) // (b9,c) by A40, AFF_1: 4;

        then LIN (b9,a9,c) by AFF_1:def 1;

        then c in N by A3, A9, A10, A20, AFF_1: 25;

        hence contradiction by A6, A7, A8, AFF_1: 45;

      end;

       A42:

      now

        assume o = x;

        then N = T by A3, A9, A26, A28, A32, A39, A41, AFF_1: 18;

        then N = K by A11, A29, A27, AFF_1: 45;

        hence contradiction by A4, A7, A8, A25, AFF_1: 45;

      end;

      

       A43: (a,c9) // (x,a9) by A25, A29, A26, A27, A32, AFF_1: 39;

       A44:

      now

        assume o = a9;

        then LIN (a9,b,x) by A36, A37, A34, A38, AFF_1: 21;

        then (a9,b) // (a9,x) by AFF_1:def 1;

        then (b,a9) // (x,a9) by AFF_1: 4;

        then (a,b9) // (x,a9) by A12, A14, AFF_1: 5;

        then (a,b9) // (a,c9) by A43, A41, AFF_1: 5;

        then LIN (a,b9,c9) by AFF_1:def 1;

        then LIN (b9,c9,a) by AFF_1: 6;

        then a in N by A3, A10, A11, A23, AFF_1: 25;

        hence contradiction by A4, A7, A8, AFF_1: 45;

      end;

      (c,b9) // (x,b9) by A40, AFF_1: 4;

      then

       A45: (b,c9) // (x,b9) by A13, A15, AFF_1: 5;

      

       A46: a <> b9 by A4, A7, A8, A10, AFF_1: 45;

       not (a,b9) // D

      proof

        assume (a,b9) // D;

        then (b,a9) // D by A12, A46, AFF_1: 32;

        then a9 in D by A36, A34, AFF_1: 23;

        then b in T by A26, A28, A32, A36, A37, A34, A41, AFF_1: 18;

        then (b,a9) // (a,c9) by A25, A29, A26, A27, AFF_1: 39;

        then (a,b9) // (a,c9) by A12, A14, AFF_1: 5;

        then LIN (a,b9,c9) by AFF_1:def 1;

        then LIN (b9,c9,a) by AFF_1: 6;

        then a in N by A3, A10, A11, A23, AFF_1: 25;

        hence contradiction by A4, A7, A8, AFF_1: 45;

      end;

      then

      consider y such that

       A47: y in D and

       A48: LIN (a,b9,y) by A36, AFF_1: 59;

      

       A49: LIN (a,y,a) by AFF_1: 7;

      

       A50: b9 <> x

      proof

        assume b9 = x;

        then (a,c9) // (a9,b9) by A25, A29, A26, A27, A32, AFF_1: 39;

        then (a,c9) // N by A3, A9, A10, A20, AFF_1: 27;

        then (c9,a) // N by AFF_1: 34;

        then a in N by A3, A11, AFF_1: 23;

        hence contradiction by A4, A7, A8, AFF_1: 45;

      end;

       A51:

      now

        assume o = b9;

        then LIN (b9,x,b) by A36, A37, A34, A38, AFF_1: 21;

        then (b9,x) // (b9,b) by AFF_1:def 1;

        then (x,b9) // (b,b9) by AFF_1: 4;

        then (b,c9) // (b,b9) by A45, A50, AFF_1: 5;

        then LIN (b,c9,b9) by AFF_1:def 1;

        then LIN (b9,c9,b) by AFF_1: 6;

        then b in N by A3, A10, A11, A23, AFF_1: 25;

        hence contradiction by A5, A7, A8, AFF_1: 45;

      end;

       A52:

      now

        assume o = y;

        then LIN (b9,o,a) by A48, AFF_1: 6;

        then a in N by A3, A10, A39, A51, AFF_1: 25;

        hence contradiction by A4, A7, A8, AFF_1: 45;

      end;

      

       A53: b <> c9 by A5, A7, A8, A11, AFF_1: 45;

       A54:

      now

        assume o = c9;

        then D // C by A13, A15, A53, A16, A30, A36, A34, A38, AFF_1: 38;

        then b in C by A31, A37, A34, AFF_1: 45;

        then LIN (c,b,b9) by A16, A30, AFF_1: 21;

        then b9 in M by A2, A5, A6, A21, AFF_1: 25;

        hence contradiction by A7, A8, A10, AFF_1: 45;

      end;

       LIN (b9,a,y) by A48, AFF_1: 6;

      then (b9,a) // (b9,y) by AFF_1:def 1;

      then (a,b9) // (y,b9) by AFF_1: 4;

      then

       A55: (y,b9) // (b,a9) by A12, A46, AFF_1: 5;

      o <> b by A5, A7, A8, A39, AFF_1: 45;

      then (y,c9) // (x,a9) by A1, A3, A9, A10, A11, A36, A37, A34, A38, A39, A45, A47, A55, A35, A51, A44, A54, A42, A52;

      then (y,c9) // (a,c9) by A43, A41, AFF_1: 5;

      then (c9,y) // (c9,a) by AFF_1: 4;

      then LIN (c9,y,a) by AFF_1:def 1;

      then

       A56: LIN (a,y,c9) by AFF_1: 6;

       LIN (a,y,b9) by A48, AFF_1: 6;

      then a in D or a in N by A3, A10, A11, A23, A47, A56, A49, AFF_1: 8, AFF_1: 25;

      then D // N by A2, A4, A5, A7, A8, A18, A36, A34, AFF_1: 18, AFF_1: 45;

      hence contradiction by A38, A39, A35, AFF_1: 45;

    end;

    theorem :: AFF_2:10

    

     Th10: AP is satisfying_PPAP iff AP is Pappian & AP is satisfying_pap

    proof

      

       A1: AP is Pappian & AP is satisfying_pap implies AP is satisfying_PPAP

      proof

        assume that

         A2: AP is Pappian and

         A3: AP is satisfying_pap;

        thus AP is satisfying_PPAP

        proof

          let M, N, a, b, c, a9, b9, c9;

          assume that

           A4: M is being_line and

           A5: N is being_line and

           A6: a in M and

           A7: b in M and

           A8: c in M and

           A9: a9 in N and

           A10: b9 in N and

           A11: c9 in N and

           A12: (a,b9) // (b,a9) and

           A13: (b,c9) // (c,b9);

          now

            assume

             A14: M <> N;

            assume

             A15: not thesis;

            now

              assume not M // N;

              then

              consider o such that

               A16: o in M and

               A17: o in N by A4, A5, AFF_1: 58;

              

               A18: o <> a

              proof

                assume

                 A19: o = a;

                then (o,b9) // (a9,b) by A12, AFF_1: 4;

                then o = b9 or b in N by A5, A9, A10, A17, AFF_1: 48;

                then o = b9 or o = b by A4, A5, A7, A14, A16, A17, AFF_1: 18;

                then (c,o) // (b,c9) or (o,c9) // (b9,c) by A13, AFF_1: 4;

                then c9 in M or c = o or c in N or o = c9 by A4, A5, A7, A8, A10, A11, A16, A17, AFF_1: 48;

                then o = c or o = c9 by A4, A5, A8, A11, A14, A16, A17, AFF_1: 18;

                hence contradiction by A5, A9, A11, A15, A17, A19, AFF_1: 3, AFF_1: 51;

              end;

              

               A20: o <> b

              proof

                assume

                 A21: o = b;

                then (o,c9) // (b9,c) by A13, AFF_1: 4;

                then o = c9 or c in N by A5, A10, A11, A17, AFF_1: 48;

                then

                 A22: o = c9 or o = c by A4, A5, A8, A14, A16, A17, AFF_1: 18;

                (o,a9) // (b9,a) by A12, A21, AFF_1: 4;

                then o = a9 or a in N by A5, A9, A10, A17, AFF_1: 48;

                hence contradiction by A4, A5, A6, A8, A14, A15, A16, A17, A18, A22, AFF_1: 3, AFF_1: 18, AFF_1: 51;

              end;

              

               A23: o <> c9

              proof

                assume

                 A24: o = c9;

                then b9 in M by A4, A7, A8, A13, A16, A20, AFF_1: 48;

                then (a,o) // (b,a9) by A4, A5, A10, A12, A14, A16, A17, AFF_1: 18;

                then a9 in M by A4, A6, A7, A16, A18, AFF_1: 48;

                hence contradiction by A4, A6, A8, A15, A16, A24, AFF_1: 51;

              end;

              

               A25: o <> c

              proof

                assume

                 A26: o = c;

                then (o,b9) // (c9,b) by A13, AFF_1: 4;

                then o = b9 or b in N by A5, A10, A11, A17, AFF_1: 48;

                then a9 in M by A4, A5, A6, A7, A9, A12, A16, A17, A18, A20, AFF_1: 18, AFF_1: 48;

                then a9 = o by A4, A5, A9, A14, A16, A17, AFF_1: 18;

                hence contradiction by A15, A26, AFF_1: 3;

              end;

              

               A27: o <> a9

              proof

                assume

                 A28: o = a9;

                then (o,b) // (a,b9) by A12, AFF_1: 4;

                then b9 in M by A4, A6, A7, A16, A20, AFF_1: 48;

                then o = b9 by A4, A5, A10, A14, A16, A17, AFF_1: 18;

                then (c,o) // (b,c9) by A13, AFF_1: 4;

                then c9 in M by A4, A7, A8, A16, A25, AFF_1: 48;

                hence contradiction by A4, A6, A8, A15, A16, A28, AFF_1: 51;

              end;

              o <> b9

              proof

                assume

                 A29: o = b9;

                then (o,c) // (b,c9) by A13, AFF_1: 4;

                then

                 A30: c9 in M by A4, A7, A8, A16, A25, AFF_1: 48;

                a9 in M by A4, A6, A7, A12, A16, A18, A29, AFF_1: 48;

                hence contradiction by A4, A6, A8, A15, A30, AFF_1: 51;

              end;

              hence thesis by A2, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A16, A17, A18, A20, A25, A27, A23;

            end;

            hence thesis by A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14;

          end;

          hence thesis by A4, A6, A8, A9, A11, AFF_1: 51;

        end;

      end;

      thus thesis by A1;

    end;

    theorem :: AFF_2:11

    AP is Pappian implies AP is Desarguesian

    proof

      assume

       A1: AP is Pappian;

      then AP is satisfying_pap by Th9;

      then

       A2: AP is satisfying_PPAP by A1, Th10;

      let A, P, C, o, a, b, c, a9, b9, c9;

      assume that

       A3: o in A and

       A4: o in P and

       A5: o in C and

       A6: o <> a and

       A7: o <> b and o <> c and

       A8: a in A and

       A9: a9 in A and

       A10: b in P and

       A11: b9 in P and

       A12: c in C and

       A13: c9 in C and

       A14: A is being_line and

       A15: P is being_line and

       A16: C is being_line and

       A17: A <> P and

       A18: A <> C and

       A19: (a,b) // (a9,b9) and

       A20: (a,c) // (a9,c9);

      assume

       A21: not (b,c) // (b9,c9);

      then

       A22: b <> c by AFF_1: 3;

      

       A23: a <> c by A3, A5, A6, A8, A12, A14, A16, A18, AFF_1: 18;

      

       A24: not b in C

      proof

        assume

         A25: b in C;

        then b9 in C by A4, A5, A7, A10, A11, A15, A16, AFF_1: 18;

        hence contradiction by A12, A13, A16, A21, A25, AFF_1: 51;

      end;

      

       A26: a <> b by A3, A4, A6, A8, A10, A14, A15, A17, AFF_1: 18;

      

       A27: a <> a9

      proof

        assume

         A28: a = a9;

        then LIN (a,c,c9) by A20, AFF_1:def 1;

        then LIN (c,c9,a) by AFF_1: 6;

        then

         A29: c = c9 or a in C by A12, A13, A16, AFF_1: 25;

         LIN (a,b,b9) by A19, A28, AFF_1:def 1;

        then LIN (b,b9,a) by AFF_1: 6;

        then b = b9 or a in P by A10, A11, A15, AFF_1: 25;

        hence contradiction by A3, A4, A5, A6, A8, A14, A15, A16, A17, A18, A21, A29, AFF_1: 2, AFF_1: 18;

      end;

      set M = ( Line (b9,c9)), N = ( Line (a9,b9)), D = ( Line (a9,c9));

      

       A30: a9 <> b9

      proof

        

         A31: (a9,c9) // (c,a) by A20, AFF_1: 4;

        assume

         A32: a9 = b9;

        then a9 in C by A3, A4, A5, A9, A11, A14, A15, A17, AFF_1: 18;

        then a in C or a9 = c9 by A12, A13, A16, A31, AFF_1: 48;

        hence contradiction by A3, A5, A6, A8, A14, A16, A18, A21, A32, AFF_1: 3, AFF_1: 18;

      end;

      then

       A33: N is being_line by AFF_1: 24;

      

       A34: a9 <> c9

      proof

        assume a9 = c9;

        then

         A35: a9 in P by A3, A4, A5, A9, A13, A14, A16, A18, AFF_1: 18;

        (a9,b9) // (b,a) by A19, AFF_1: 4;

        then a in P by A10, A11, A15, A30, A35, AFF_1: 48;

        hence contradiction by A3, A4, A6, A8, A14, A15, A17, AFF_1: 18;

      end;

      

       A36: not LIN (a9,b9,c9)

      proof

        assume

         A37: LIN (a9,b9,c9);

        then (a9,b9) // (a9,c9) by AFF_1:def 1;

        then (a9,b9) // (a,c) by A20, A34, AFF_1: 5;

        then (a,b) // (a,c) by A19, A30, AFF_1: 5;

        then LIN (a,b,c) by AFF_1:def 1;

        then LIN (b,c,a) by AFF_1: 6;

        then (b,c) // (b,a) by AFF_1:def 1;

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

        then

         A38: (b,c) // (a9,b9) by A19, A26, AFF_1: 5;

         LIN (b9,c9,a9) by A37, AFF_1: 6;

        then (b9,c9) // (b9,a9) by AFF_1:def 1;

        then (b9,c9) // (a9,b9) by AFF_1: 4;

        hence contradiction by A21, A30, A38, AFF_1: 5;

      end;

      

       A39: not LIN (a,b,c)

      proof

        assume LIN (a,b,c);

        then (a,b) // (a,c) by AFF_1:def 1;

        then (a,b) // (a9,c9) by A20, A23, AFF_1: 5;

        then (a9,b9) // (a9,c9) by A19, A26, AFF_1: 5;

        hence contradiction by A36, AFF_1:def 1;

      end;

       A40:

      now

         LIN (o,a,a9) by A3, A8, A9, A14, AFF_1: 21;

        then (o,a) // (o,a9) by AFF_1:def 1;

        then

         A41: (a9,o) // (a,o) by AFF_1: 4;

        set M = ( Line (b,c)), N = ( Line (a,b)), D = ( Line (a,c));

        

         A42: N is being_line by A26, AFF_1: 24;

        M is being_line by A22, AFF_1: 24;

        then

        consider K such that

         A43: o in K and

         A44: M // K by AFF_1: 49;

        

         A45: K is being_line by A44, AFF_1: 36;

        

         A46: a in N by A26, AFF_1: 24;

        

         A47: b in N by A26, AFF_1: 24;

        

         A48: b in M & c in M by A22, AFF_1: 24;

         not N // K

        proof

          assume N // K;

          then N // M by A44, AFF_1: 44;

          then c in N by A48, A47, AFF_1: 45;

          hence contradiction by A39, A42, A46, A47, AFF_1: 21;

        end;

        then

        consider p such that

         A49: p in N and

         A50: p in K by A42, A45, AFF_1: 58;

        

         A51: (b,c) // (p,o) by A48, A43, A44, A50, AFF_1: 39;

        

         A52: o <> p

        proof

          assume o = p;

          then LIN (o,a,b) by A42, A46, A47, A49, AFF_1: 21;

          then b in A by A3, A6, A8, A14, AFF_1: 25;

          hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1: 18;

        end;

        set R = ( Line (a9,p));

        

         A53: p <> a9

        proof

          assume p = a9;

          then b in A by A8, A9, A14, A27, A42, A46, A47, A49, AFF_1: 18;

          hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1: 18;

        end;

        then

         A54: R is being_line by AFF_1: 24;

        D is being_line by A23, AFF_1: 24;

        then

        consider T such that

         A55: p in T and

         A56: D // T by AFF_1: 49;

        

         A57: a in D & c in D by A23, AFF_1: 24;

        

         A58: not C // T

        proof

          assume C // T;

          then C // D by A56, AFF_1: 44;

          then a in C by A12, A57, AFF_1: 45;

          hence contradiction by A3, A5, A6, A8, A14, A16, A18, AFF_1: 18;

        end;

        T is being_line by A56, AFF_1: 36;

        then

        consider q such that

         A59: q in C and

         A60: q in T by A16, A58, AFF_1: 58;

        

         A61: (p,q) // (a,c) by A57, A55, A56, A60, AFF_1: 39;

        then

         A62: (b,q) // (a,o) by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51;

        

         A63: a9 in R & p in R by A53, AFF_1: 24;

        assume not (b,c) // A;

        then

         A64: K <> A by A48, A44, AFF_1: 40;

         not (b,q) // R

        proof

          assume (b,q) // R;

          then

           A65: (a,o) // R by A24, A59, A62, AFF_1: 32;

          (a,o) // A by A3, A8, A14, AFF_1: 40, AFF_1: 41;

          then p in A by A6, A9, A63, A65, AFF_1: 45, AFF_1: 53;

          hence contradiction by A3, A14, A43, A45, A50, A52, A64, AFF_1: 18;

        end;

        then

        consider r such that

         A66: r in R and

         A67: LIN (b,q,r) by A54, AFF_1: 59;

         A68:

        now

          assume r = q;

          then (b,r) // (a,o) by A2, A5, A12, A16, A42, A46, A47, A49, A59, A51, A61;

          then

           A69: (r,b) // (o,a) by AFF_1: 4;

           LIN (o,a,a9) by A3, A8, A9, A14, AFF_1: 21;

          then (o,a) // (o,a9) by AFF_1:def 1;

          hence (r,b) // (o,a9) by A6, A69, AFF_1: 5;

        end;

         LIN (q,r,b) by A67, AFF_1: 6;

        then (q,r) // (q,b) by AFF_1:def 1;

        then (r,q) // (b,q) by AFF_1: 4;

        then (r,q) // (a,o) by A24, A59, A62, AFF_1: 5;

        then

         A70: (a9,o) // (r,q) by A6, A41, AFF_1: 5;

         LIN (b,a,p) by A42, A46, A47, A49, AFF_1: 21;

        then (b,a) // (b,p) by AFF_1:def 1;

        then (a,b) // (p,b) by AFF_1: 4;

        then

         A71: (p,b) // (a9,b9) by A19, A26, AFF_1: 5;

         LIN (r,b,q) by A67, AFF_1: 6;

        then (r,b) // (r,q) by AFF_1:def 1;

        then (a9,o) // (r,b) by A70, A68, AFF_1: 4, AFF_1: 5;

        then

         A72: (p,o) // (r,b9) by A2, A4, A10, A11, A15, A54, A63, A66, A71;

        (p,q) // (a9,c9) by A20, A23, A61, AFF_1: 5;

        then

         A73: (p,o) // (r,c9) by A2, A5, A13, A16, A59, A54, A63, A66, A70;

        then (r,c9) // (r,b9) by A52, A72, AFF_1: 5;

        then LIN (r,c9,b9) by AFF_1:def 1;

        then LIN (c9,b9,r) by AFF_1: 6;

        then (c9,b9) // (c9,r) by AFF_1:def 1;

        then

         A74: (r,c9) // (b9,c9) by AFF_1: 4;

        (b,c) // (r,c9) by A52, A51, A73, AFF_1: 5;

        then r = c9 by A21, A74, AFF_1: 5;

        then (p,o) // (b9,c9) by A72, AFF_1: 4;

        hence contradiction by A21, A52, A51, AFF_1: 5;

      end;

      

       A75: b9 in N by A30, AFF_1: 24;

      

       A76: b9 <> c9 by A21, AFF_1: 3;

      then

       A77: b9 in M & c9 in M by AFF_1: 24;

      M is being_line by A76, AFF_1: 24;

      then

      consider K such that

       A78: o in K and

       A79: M // K by AFF_1: 49;

      

       A80: K is being_line by A79, AFF_1: 36;

      

       A81: a9 in N by A30, AFF_1: 24;

       not N // K

      proof

        assume N // K;

        then N // M by A79, AFF_1: 44;

        then c9 in N by A77, A75, AFF_1: 45;

        hence contradiction by A36, A33, A81, A75, AFF_1: 21;

      end;

      then

      consider p such that

       A82: p in N and

       A83: p in K by A33, A80, AFF_1: 58;

      

       A84: o <> a9

      proof

        assume

         A85: o = a9;

        (a9,b9) // (b,a) by A19, AFF_1: 4;

        then a in P by A4, A10, A11, A15, A30, A85, AFF_1: 48;

        hence contradiction by A3, A4, A6, A8, A14, A15, A17, AFF_1: 18;

      end;

      

       A86: o <> p

      proof

        assume o = p;

        then LIN (o,a9,b9) by A33, A81, A75, A82, AFF_1: 21;

        then

         A87: b9 in A by A3, A9, A14, A84, AFF_1: 25;

        (a9,b9) // (a,b) by A19, AFF_1: 4;

        then b in A by A8, A9, A14, A30, A87, AFF_1: 48;

        hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1: 18;

      end;

      D is being_line by A34, AFF_1: 24;

      then

      consider T such that

       A88: p in T and

       A89: D // T by AFF_1: 49;

      

       A90: T is being_line by A89, AFF_1: 36;

      

       A91: a9 in D & c9 in D by A34, AFF_1: 24;

       not C // T

      proof

        assume C // T;

        then C // D by A89, AFF_1: 44;

        then a9 in C by A13, A91, AFF_1: 45;

        hence contradiction by A3, A5, A9, A14, A16, A18, A84, AFF_1: 18;

      end;

      then

      consider q such that

       A92: q in C and

       A93: q in T by A16, A90, AFF_1: 58;

      

       A94: (b9,c9) // (p,o) by A77, A78, A79, A83, AFF_1: 39;

      

       A95: o <> b9

      proof

        assume

         A96: o = b9;

        (b9,a9) // (a,b) by A19, AFF_1: 4;

        then b in A by A3, A8, A9, A14, A30, A96, AFF_1: 48;

        hence contradiction by A3, A4, A7, A10, A14, A15, A17, AFF_1: 18;

      end;

      

       A97: b9 <> q

      proof

        assume b9 = q;

        then P = C by A4, A5, A11, A15, A16, A95, A92, AFF_1: 18;

        hence contradiction by A10, A11, A12, A13, A15, A21, AFF_1: 51;

      end;

      set R = ( Line (a,p));

      

       A98: p <> a

      proof

        assume p = a;

        then b9 in A by A8, A9, A14, A27, A33, A81, A75, A82, AFF_1: 18;

        hence contradiction by A3, A4, A11, A14, A15, A17, A95, AFF_1: 18;

      end;

      then

       A99: R is being_line by AFF_1: 24;

      

       A100: (p,q) // (a9,c9) by A91, A88, A89, A93, AFF_1: 39;

      then

       A101: (b9,q) // (a9,o) by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94;

      

       A102: a in R & p in R by A98, AFF_1: 24;

       not (b9,c9) // A by A14, A21, A40, AFF_1: 31;

      then

       A103: K <> A by A77, A79, AFF_1: 40;

       not (b9,q) // R

      proof

        assume (b9,q) // R;

        then

         A104: (a9,o) // R by A101, A97, AFF_1: 32;

        (a9,o) // A by A3, A9, A14, AFF_1: 40, AFF_1: 41;

        then p in A by A8, A84, A102, A104, AFF_1: 45, AFF_1: 53;

        hence contradiction by A3, A14, A78, A80, A83, A86, A103, AFF_1: 18;

      end;

      then

      consider r such that

       A105: r in R and

       A106: LIN (b9,q,r) by A99, AFF_1: 59;

       A107:

      now

        assume r = q;

        then (b9,r) // (a9,o) by A2, A5, A13, A16, A33, A81, A75, A82, A92, A94, A100;

        then

         A108: (r,b9) // (o,a9) by AFF_1: 4;

         LIN (o,a9,a) by A3, A8, A9, A14, AFF_1: 21;

        then (o,a9) // (o,a) by AFF_1:def 1;

        hence (r,b9) // (o,a) by A84, A108, AFF_1: 5;

      end;

       LIN (b9,a9,p) by A33, A81, A75, A82, AFF_1: 21;

      then (b9,a9) // (b9,p) by AFF_1:def 1;

      then (p,b9) // (a9,b9) by AFF_1: 4;

      then

       A109: (p,b9) // (a,b) by A19, A30, AFF_1: 5;

       LIN (o,a,a9) by A3, A8, A9, A14, AFF_1: 21;

      then (o,a) // (o,a9) by AFF_1:def 1;

      then

       A110: (a,o) // (a9,o) by AFF_1: 4;

       LIN (q,r,b9) by A106, AFF_1: 6;

      then (q,r) // (q,b9) by AFF_1:def 1;

      then (r,q) // (b9,q) by AFF_1: 4;

      then (r,q) // (a9,o) by A101, A97, AFF_1: 5;

      then

       A111: (a,o) // (r,q) by A84, A110, AFF_1: 5;

       LIN (r,b9,q) by A106, AFF_1: 6;

      then (r,b9) // (r,q) by AFF_1:def 1;

      then (a,o) // (r,b9) by A111, A107, AFF_1: 4, AFF_1: 5;

      then

       A112: (p,o) // (r,b) by A2, A4, A10, A11, A15, A99, A102, A105, A109;

      (p,q) // (a,c) by A20, A34, A100, AFF_1: 5;

      then

       A113: (p,o) // (r,c) by A2, A5, A12, A16, A92, A99, A102, A105, A111;

      then (r,c) // (r,b) by A86, A112, AFF_1: 5;

      then LIN (r,c,b) by AFF_1:def 1;

      then LIN (c,b,r) by AFF_1: 6;

      then (c,b) // (c,r) by AFF_1:def 1;

      then

       A114: (b,c) // (r,c) by AFF_1: 4;

      (b9,c9) // (r,c) by A86, A94, A113, AFF_1: 5;

      then r = c by A21, A114, AFF_1: 5;

      then (b,c) // (p,o) by A112, AFF_1: 4;

      hence contradiction by A21, A86, A94, AFF_1: 5;

    end;

    theorem :: AFF_2:12

    AP is Desarguesian implies AP is Moufangian

    proof

      assume

       A1: AP is Desarguesian;

      let K, o, a, b, c, a9, b9, c9;

      assume that

       A2: K is being_line and

       A3: o in K and

       A4: c in K & c9 in K and

       A5: not a in K and

       A6: o <> c and

       A7: a <> b and

       A8: LIN (o,a,a9) and

       A9: LIN (o,b,b9) and

       A10: (a,b) // (a9,b9) & (a,c) // (a9,c9) and

       A11: (a,b) // K;

      set A = ( Line (o,a)), P = ( Line (o,b));

      

       A12: o in A by A3, A5, AFF_1: 24;

       A13:

      now

        assume

         A14: o = b;

        (b,a) // K by A11, AFF_1: 34;

        hence contradiction by A2, A3, A5, A14, AFF_1: 23;

      end;

      then

       A15: b in P by AFF_1: 24;

      

       A16: a in A by A3, A5, AFF_1: 24;

      

       A17: A is being_line by A3, A5, AFF_1: 24;

      

       A18: A <> P

      proof

        assume A = P;

        then (a,b) // A by A17, A16, A15, AFF_1: 40, AFF_1: 41;

        hence contradiction by A3, A5, A7, A11, A12, A16, AFF_1: 45, AFF_1: 53;

      end;

      

       A19: P is being_line & o in P by A13, AFF_1: 24;

      then

       A20: b9 in P by A9, A13, A15, AFF_1: 25;

      a9 in A by A3, A5, A8, A17, A12, A16, AFF_1: 25;

      hence thesis by A1, A2, A3, A4, A5, A6, A10, A13, A17, A12, A16, A19, A15, A20, A18;

    end;

    theorem :: AFF_2:13

    

     Th13: AP is satisfying_TDES_1 implies AP is satisfying_des_1

    proof

      assume

       A1: AP is satisfying_TDES_1;

      let A, P, C, a, b, c, a9, b9, c9;

      assume that

       A2: A // P and

       A3: a in A and

       A4: a9 in A and

       A5: b in P and

       A6: b9 in P and

       A7: c in C and

       A8: c9 in C and

       A9: A is being_line and

       A10: P is being_line and

       A11: C is being_line and

       A12: A <> P and

       A13: A <> C and

       A14: (a,b) // (a9,b9) and

       A15: (a,c) // (a9,c9) and

       A16: (b,c) // (b9,c9) and

       A17: not LIN (a,b,c) and

       A18: c <> c9;

      set P9 = ( Line (a,b)), C9 = ( Line (a9,b9));

      

       A19: a9 <> b9 by A2, A4, A6, A12, AFF_1: 45;

      then

       A20: a9 in C9 by AFF_1: 24;

      

       A21: a9 <> c9

      proof

        assume a9 = c9;

        then (b,c) // (a9,b9) by A16, AFF_1: 4;

        then (a,b) // (b,c) by A14, A19, AFF_1: 5;

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

        then LIN (b,a,c) by AFF_1:def 1;

        hence contradiction by A17, AFF_1: 6;

      end;

      

       A22: not c9 in A

      proof

        assume

         A23: c9 in A;

        (a9,c9) // (a,c) by A15, AFF_1: 4;

        then c in A by A3, A4, A9, A21, A23, AFF_1: 48;

        hence contradiction by A7, A8, A9, A11, A13, A18, A23, AFF_1: 18;

      end;

      

       A24: C9 is being_line by A19, AFF_1: 24;

      assume

       A25: not A // C;

      then

      consider o such that

       A26: o in A and

       A27: o in C by A9, A11, AFF_1: 58;

      

       A28: LIN (o,c9,c) by A7, A8, A11, A27, AFF_1: 21;

      

       A29: a <> a9

      proof

        assume

         A30: a = a9;

        then LIN (a,c,c9) by A15, AFF_1:def 1;

        then

         A31: LIN (c,c9,a) by AFF_1: 6;

         LIN (a,b,b9) by A14, A30, AFF_1:def 1;

        then LIN (b,b9,a) by AFF_1: 6;

        then b = b9 or a in P by A5, A6, A10, AFF_1: 25;

        then LIN (b,c,c9) by A2, A3, A12, A16, AFF_1: 45, AFF_1:def 1;

        then

         A32: LIN (c,c9,b) by AFF_1: 6;

         LIN (c,c9,c) by AFF_1: 7;

        hence contradiction by A17, A18, A31, A32, AFF_1: 8;

      end;

      

       A33: o <> a9

      proof

        assume

         A34: o = a9;

        (a9,c9) // (c,a) by A15, AFF_1: 4;

        then a in C by A7, A8, A11, A27, A21, A34, AFF_1: 48;

        hence contradiction by A3, A4, A9, A11, A13, A27, A29, A34, AFF_1: 18;

      end;

      

       A35: a <> b by A17, AFF_1: 7;

      then

       A36: P9 is being_line by AFF_1: 24;

      consider N such that

       A37: c9 in N and

       A38: A // N by A9, AFF_1: 49;

      

       A39: b9 in C9 by A19, AFF_1: 24;

      

       A40: not N // C9

      proof

        assume N // C9;

        then A // C9 by A38, AFF_1: 44;

        then b9 in A by A4, A39, A20, AFF_1: 45;

        hence contradiction by A2, A6, A12, AFF_1: 45;

      end;

      N is being_line by A38, AFF_1: 36;

      then

      consider q such that

       A41: q in N and

       A42: q in C9 by A24, A40, AFF_1: 58;

      

       A43: (c9,q) // A by A37, A38, A41, AFF_1: 40;

      

       A44: c9 <> q

      proof

        assume c9 = q;

        then LIN (a9,b9,c9) by A24, A39, A20, A42, AFF_1: 21;

        then (a9,b9) // (a9,c9) by AFF_1:def 1;

        then (a9,b9) // (a,c) by A15, A21, AFF_1: 5;

        then (a,b) // (a,c) by A14, A19, AFF_1: 5;

        hence contradiction by A17, AFF_1:def 1;

      end;

      

       A45: (c9,a9) // (c,a) by A15, AFF_1: 4;

      

       A46: (c,b) // (c9,b9) by A16, AFF_1: 4;

      

       A47: a in P9 by A35, AFF_1: 24;

      

       A48: b <> c by A17, AFF_1: 7;

      

       A49: not c in P

      proof

        assume

         A50: c in P;

        then c9 in P by A5, A6, A10, A16, A48, AFF_1: 48;

        hence contradiction by A2, A7, A8, A10, A11, A18, A25, A50, AFF_1: 18;

      end;

       not P // C by A2, A25, AFF_1: 44;

      then

      consider s such that

       A51: s in P and

       A52: s in C by A10, A11, AFF_1: 58;

      

       A53: LIN (s,c,c9) by A7, A8, A11, A52, AFF_1: 21;

      

       A54: b <> b9

      proof

        assume b = b9;

        then (b,a) // (b,a9) by A14, AFF_1: 4;

        then LIN (b,a,a9) by AFF_1:def 1;

        then LIN (a,a9,b) by AFF_1: 6;

        then b in A by A3, A4, A9, A29, AFF_1: 25;

        hence contradiction by A2, A5, A12, AFF_1: 45;

      end;

      

       A55: s <> b

      proof

        assume

         A56: s = b;

        (b,c) // (c9,b9) by A16, AFF_1: 4;

        then b9 in C by A7, A8, A11, A48, A52, A56, AFF_1: 48;

        hence contradiction by A2, A5, A6, A10, A11, A25, A54, A52, A56, AFF_1: 18;

      end;

      consider M such that

       A57: c in M and

       A58: A // M by A9, AFF_1: 49;

      

       A59: M is being_line by A58, AFF_1: 36;

      

       A60: b in P9 by A35, AFF_1: 24;

       not M // P9

      proof

        assume M // P9;

        then A // P9 by A58, AFF_1: 44;

        then b in A by A3, A60, A47, AFF_1: 45;

        hence contradiction by A2, A5, A12, AFF_1: 45;

      end;

      then

      consider p such that

       A61: p in M and

       A62: p in P9 by A59, A36, AFF_1: 58;

      M // P by A2, A58, AFF_1: 44;

      then

       A63: (c,p) // P by A57, A61, AFF_1: 40;

      

       A64: M // N by A58, A38, AFF_1: 44;

      then

       A65: (c,p) // (c9,q) by A57, A37, A61, A41, AFF_1: 39;

       A66:

      now

        assume p = q;

        then M = N by A64, A61, A41, AFF_1: 45;

        hence contradiction by A7, A8, A11, A18, A25, A57, A58, A37, A59, AFF_1: 18;

      end;

      

       A67: P9 // C9 by A14, A35, A19, AFF_1: 37;

      then

       A68: (p,b) // (q,b9) by A60, A39, A62, A42, AFF_1: 39;

      

       A69: (q,a9) // (p,a) by A47, A20, A67, A62, A42, AFF_1: 39;

      (c9,q) // (c,p) by A57, A37, A64, A61, A41, AFF_1: 39;

      then LIN (o,q,p) by A1, A3, A4, A9, A26, A28, A22, A45, A69, A43, A44, A33;

      then

       A70: LIN (p,q,o) by AFF_1: 6;

      c <> p by A17, A36, A60, A47, A62, AFF_1: 21;

      then LIN (s,p,q) by A1, A5, A6, A10, A51, A53, A63, A68, A49, A55, A65, A46;

      then

       A71: LIN (p,q,s) by AFF_1: 6;

       LIN (p,q,p) by AFF_1: 7;

      then o = s or p in C by A11, A27, A52, A70, A71, A66, AFF_1: 8, AFF_1: 25;

      then c in P9 by A2, A7, A11, A12, A25, A26, A57, A58, A59, A61, A62, A51, AFF_1: 18, AFF_1: 45;

      hence contradiction by A17, A36, A60, A47, AFF_1: 21;

    end;

    theorem :: AFF_2:14

    AP is Moufangian implies AP is translational

    proof

      assume AP is Moufangian;

      then AP is satisfying_des_1 by Th3, Th13;

      hence thesis by Th7;

    end;

    theorem :: AFF_2:15

    AP is translational implies AP is satisfying_pap

    proof

      assume

       A1: AP is translational;

      let M, N, a, b, c, a9, b9, c9;

      assume that

       A2: M is being_line and

       A3: N is being_line and

       A4: a in M and

       A5: b in M and

       A6: c in M and

       A7: M // N and

       A8: M <> N and

       A9: a9 in N and

       A10: b9 in N and

       A11: c9 in N and

       A12: (a,b9) // (b,a9) and

       A13: (b,c9) // (c,b9);

      set A = ( Line (a,b9)), A9 = ( Line (b,a9)), P = ( Line (b,c9)), P9 = ( Line (c,b9));

      

       A14: c <> b9 by A6, A7, A8, A10, AFF_1: 45;

      then

       A15: c in P9 & b9 in P9 by AFF_1: 24;

      

       A16: b <> c9 by A5, A7, A8, A11, AFF_1: 45;

      then

       A17: P is being_line & b in P by AFF_1: 24;

      

       A18: P9 is being_line by A14, AFF_1: 24;

      then

      consider C9 such that

       A19: a in C9 and

       A20: P9 // C9 by AFF_1: 49;

      

       A21: C9 is being_line by A20, AFF_1: 36;

      assume

       A22: not thesis;

       A23:

      now

        assume

         A24: a = c;

        then (b,c9) // (b,a9) by A12, A13, A14, AFF_1: 5;

        then LIN (b,c9,a9) by AFF_1:def 1;

        then LIN (a9,c9,b) by AFF_1: 6;

        then a9 = c9 or b in N by A3, A9, A11, AFF_1: 25;

        hence contradiction by A5, A7, A8, A22, A24, AFF_1: 2, AFF_1: 45;

      end;

      

       A25: P9 <> C9

      proof

        assume P9 = C9;

        then LIN (a,c,b9) by A18, A15, A19, AFF_1: 21;

        then b9 in M by A2, A4, A6, A23, AFF_1: 25;

        hence contradiction by A7, A8, A10, AFF_1: 45;

      end;

      

       A26: c9 in P by A16, AFF_1: 24;

      then

       A27: P9 // P by A13, A16, A14, A18, A17, A15, AFF_1: 38;

       A28:

      now

        assume

         A29: b = c;

        then LIN (b,c9,b9) by A13, AFF_1:def 1;

        then LIN (b9,c9,b) by AFF_1: 6;

        then b9 = c9 or b in N by A3, A10, A11, AFF_1: 25;

        hence contradiction by A5, A7, A8, A12, A22, A29, AFF_1: 45;

      end;

      

       A30: P9 <> P

      proof

        assume P9 = P;

        then LIN (b,c,b9) by A17, A15, AFF_1: 21;

        then b9 in M by A2, A5, A6, A28, AFF_1: 25;

        hence contradiction by A7, A8, A10, AFF_1: 45;

      end;

      

       A31: a <> b9 by A4, A7, A8, A10, AFF_1: 45;

      then

       A32: A is being_line by AFF_1: 24;

      then

      consider C such that

       A33: c in C and

       A34: A // C by AFF_1: 49;

      

       A35: C is being_line by A34, AFF_1: 36;

      

       A36: (a,b) // (b9,a9) by A4, A5, A7, A9, A10, AFF_1: 39;

      

       A37: (b9,c9) // (c,b) by A5, A6, A7, A10, A11, AFF_1: 39;

      

       A38: b <> a9 by A5, A7, A8, A9, AFF_1: 45;

      then

       A39: a9 in A9 by AFF_1: 24;

      

       A40: a in A & b9 in A by A31, AFF_1: 24;

      

       A41: A <> C

      proof

        assume A = C;

        then LIN (a,c,b9) by A32, A40, A33, AFF_1: 21;

        then b9 in M by A2, A4, A6, A23, AFF_1: 25;

        hence contradiction by A7, A8, A10, AFF_1: 45;

      end;

       not C // C9

      proof

        assume C // C9;

        then A // C9 by A34, AFF_1: 44;

        then A // P9 by A20, AFF_1: 44;

        then (b9,a) // (b9,c) by A40, A15, AFF_1: 39;

        then LIN (b9,a,c) by AFF_1:def 1;

        then LIN (a,c,b9) by AFF_1: 6;

        then b9 in M by A2, A4, A6, A23, AFF_1: 25;

        hence contradiction by A7, A8, A10, AFF_1: 45;

      end;

      then

      consider s such that

       A42: s in C and

       A43: s in C9 by A35, A21, AFF_1: 58;

      

       A44: A9 is being_line & b in A9 by A38, AFF_1: 24;

       A45:

      now

        assume

         A46: a = b;

        then LIN (a,b9,a9) by A12, AFF_1:def 1;

        then LIN (a9,b9,a) by AFF_1: 6;

        then a9 = b9 or a in N by A3, A9, A10, AFF_1: 25;

        hence contradiction by A4, A7, A8, A13, A22, A46, AFF_1: 45;

      end;

       A47:

      now

        assume a9 = b9;

        then (a9,a) // (a9,b) by A12, AFF_1: 4;

        then LIN (a9,a,b) by AFF_1:def 1;

        then LIN (a,b,a9) by AFF_1: 6;

        then a9 in M by A2, A4, A5, A45, AFF_1: 25;

        hence contradiction by A7, A8, A9, AFF_1: 45;

      end;

      

       A48: A <> A9

      proof

        assume A = A9;

        then LIN (a9,b9,a) by A32, A40, A39, AFF_1: 21;

        then a in N by A3, A9, A10, A47, AFF_1: 25;

        hence contradiction by A4, A7, A8, AFF_1: 45;

      end;

      

       A49: b <> s

      proof

        assume b = s;

        then (a,b9) // (b,c) by A40, A33, A34, A42, AFF_1: 39;

        then (b,a9) // (b,c) by A12, A31, AFF_1: 5;

        then LIN (b,a9,c) by AFF_1:def 1;

        then LIN (b,c,a9) by AFF_1: 6;

        then a9 in M by A2, A5, A6, A28, AFF_1: 25;

        hence contradiction by A7, A8, A9, AFF_1: 45;

      end;

      

       A50: A // A9 by A12, A31, A38, AFF_1: 37;

      (a,s) // (b9,c) by A15, A19, A20, A43, AFF_1: 39;

      then

       A51: (b,s) // (a9,c) by A1, A32, A40, A44, A39, A33, A34, A35, A42, A36, A48, A41, A50;

      (b9,a) // (c,s) by A40, A33, A34, A42, AFF_1: 39;

      then (c9,a) // (b,s) by A1, A18, A17, A26, A15, A19, A20, A21, A43, A37, A30, A25, A27;

      then (c9,a) // (a9,c) by A51, A49, AFF_1: 5;

      hence contradiction by A22, AFF_1: 4;

    end;