aff_3.miz



    begin

    reserve AP for AffinPlane;

    reserve a,a9,b,b9,c,c9,d,x,y,o,p,q for Element of AP;

    reserve A,C,D9,M,N,P for Subset of AP;

    definition

      let AP;

      :: AFF_3:def1

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

    end

    definition

      let AP;

      :: AFF_3:def2

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

    end

    definition

      let AP;

      :: AFF_3:def3

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

    end

    definition

      let AP;

      :: AFF_3:def4

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

    end

    definition

      let AP;

      :: AFF_3:def5

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

    end

    definition

      let AP;

      :: AFF_3:def6

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

    end

    definition

      let AP;

      :: AFF_3:def7

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

    end

    definition

      let AP;

      :: AFF_3:def8

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

    end

    theorem :: AFF_3:1

    AP is satisfying_DES1 implies AP is satisfying_DES1_1

    proof

      assume

       A1: AP is satisfying_DES1;

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

      assume that

       A2: A is being_line and

       A3: P is being_line and

       A4: C is being_line and

       A5: P <> A and

       A6: P <> C and

       A7: A <> C and

       A8: o in A and

       A9: a in A and

       A10: a9 in A and

       A11: o in P and

       A12: b in P & b9 in P and

       A13: o in C & c in C and

       A14: c9 in C and

       A15: o <> a and

       A16: o <> b and

       A17: o <> c and

       A18: p <> q and

       A19: c <> q and

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

       A21: not LIN (b9,a9,c9) and

       A22: LIN (b,a,p) and

       A23: LIN (b9,a9,p) and

       A24: LIN (b,c,q) and

       A25: LIN (b9,c9,q) and

       A26: (a,c) // (p,q);

      

       A27: LIN (o,a,a9) & LIN (b9,p,a9) by A2, A8, A9, A10, A23, AFF_1: 6, AFF_1: 21;

      set K = ( Line (b,a));

      

       A28: a in K by AFF_1: 15;

      then

       A29: K <> P by A2, A3, A5, A8, A9, A11, A15, AFF_1: 18;

      

       A30: not LIN (o,a,c)

      proof

        assume LIN (o,a,c);

        then c in A by A2, A8, A9, A15, AFF_1: 25;

        hence contradiction by A2, A4, A7, A8, A13, A17, AFF_1: 18;

      end;

      

       A31: p in K by A22, AFF_1:def 2;

      

       A32: LIN (o,c,c9) & LIN (b9,q,c9) by A4, A13, A14, A25, AFF_1: 6, AFF_1: 21;

      

       A33: b <> c & a <> p by A19, A20, A24, A26, AFF_1: 7, AFF_1: 14;

      

       A34: a9 <> c9 & b <> a by A20, A21, AFF_1: 7;

      b <> a by A20, AFF_1: 7;

      then

       A35: K is being_line by AFF_1:def 3;

      set M = ( Line (b,c));

      

       A36: c in M by AFF_1: 15;

      then

       A37: M <> P by A3, A4, A6, A11, A13, A17, AFF_1: 18;

      b <> c by A20, AFF_1: 7;

      then

       A38: M is being_line by AFF_1:def 3;

      

       A39: b in M & q in M by A24, AFF_1: 15, AFF_1:def 2;

      q <> b

      proof

        assume

         A40: q = b;

        ( not LIN (b,c,a)) & (c,a) // (q,p) by A20, A26, AFF_1: 4, AFF_1: 6;

        hence contradiction by A18, A22, A40, AFF_1: 55;

      end;

      then

       A41: q <> b9 by A3, A12, A38, A39, A37, AFF_1: 18;

      

       A42: b in K by AFF_1: 15;

      p <> b by A18, A20, A24, A26, AFF_1: 55;

      then

       A43: p <> b9 by A3, A12, A35, A42, A31, A29, AFF_1: 18;

      

       A44: not LIN (b9,p,q)

      proof

        set N = ( Line (p,q));

        

         A45: N is being_line by A18, AFF_1:def 3;

        assume LIN (b9,p,q);

        then LIN (p,q,b9) by AFF_1: 6;

        then

         A46: b9 in N by AFF_1:def 2;

        q in N & LIN (q,b9,c9) by A25, AFF_1: 6, AFF_1: 15;

        then

         A47: c9 in N by A41, A45, A46, AFF_1: 25;

        p in N & LIN (p,b9,a9) by A23, AFF_1: 6, AFF_1: 15;

        then a9 in N by A43, A45, A46, AFF_1: 25;

        hence contradiction by A21, A45, A46, A47, AFF_1: 21;

      end;

      K <> M by A20, A35, A42, A28, A36, AFF_1: 21;

      hence thesis by A1, A3, A11, A12, A16, A26, A35, A38, A42, A28, A36, A31, A39, A37, A29, A34, A30, A44, A33, A27, A32;

    end;

    theorem :: AFF_3:2

    AP is satisfying_DES1_1 implies AP is satisfying_DES1

    proof

      assume

       A1: AP is satisfying_DES1_1;

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

      assume that

       A2: A is being_line and

       A3: P is being_line and

       A4: C is being_line and

       A5: P <> A and

       A6: P <> C and

       A7: A <> C and

       A8: o in A and

       A9: a in A and

       A10: a9 in A and

       A11: o in P and

       A12: b in P and

       A13: b9 in P and

       A14: o in C and

       A15: c in C and

       A16: c9 in C and

       A17: o <> a and

       A18: o <> b and

       A19: o <> c and

       A20: p <> q and

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

       A22: not LIN (b9,a9,c9) and

       A23: a <> a9 and

       A24: LIN (b,a,p) and

       A25: LIN (b9,a9,p) and

       A26: LIN (b,c,q) and

       A27: LIN (b9,c9,q) and

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

      

       A29: a9 <> b9 by A22, AFF_1: 7;

      set M = ( Line (b,c));

      

       A30: c in M by AFF_1: 15;

      then

       A31: M <> P by A3, A4, A6, A11, A14, A15, A19, AFF_1: 18;

      

       A32: M <> P by A3, A4, A6, A11, A14, A15, A19, A30, AFF_1: 18;

      

       A33: b in M by AFF_1: 15;

      set K = ( Line (b,a));

      

       A34: a in K by AFF_1: 15;

      then

       A35: K <> P by A2, A3, A5, A8, A9, A11, A17, AFF_1: 18;

      

       A36: p in K by A24, AFF_1:def 2;

      

       A37: a9 <> c9 & b <> a by A21, A22, AFF_1: 7;

      

       A38: b <> c by A21, AFF_1: 7;

      

       A39: q in M by A26, AFF_1:def 2;

      

       A40: b9 <> c9 by A22, AFF_1: 7;

      

       A41: b in K by AFF_1: 15;

      

       A42: not LIN (o,a,c)

      proof

        assume LIN (o,a,c);

        then c in A by A2, A8, A9, A17, AFF_1: 25;

        hence contradiction by A2, A4, A7, A8, A14, A15, A19, AFF_1: 18;

      end;

      

       A43: c <> c9

      proof

        assume c = c9;

        then

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

         LIN (o,a,a9) & not LIN (o,c,a) by A2, A8, A9, A10, A42, AFF_1: 6, AFF_1: 21;

        hence contradiction by A23, A44, AFF_1: 14;

      end;

      b <> c by A21, AFF_1: 7;

      then

       A45: M is being_line by AFF_1:def 3;

      b <> a by A21, AFF_1: 7;

      then

       A46: K is being_line by AFF_1:def 3;

      

       A47: K <> P by A2, A3, A5, A8, A9, A11, A17, A34, AFF_1: 18;

       A48:

      now

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

        set A9 = ( Line (b9,a9));

        

         A49: c9 in C9 by AFF_1: 15;

        

         A50: A9 is being_line & b9 in A9 by A29, AFF_1: 15, AFF_1:def 3;

        

         A51: a9 in A9 by AFF_1: 15;

        then

         A52: A9 <> C9 by A22, A50, A49, AFF_1: 21;

        

         A53: q in C9 by A27, AFF_1:def 2;

        

         A54: p in A9 by A25, AFF_1:def 2;

        

         A55: C9 is being_line & b9 in C9 by A40, AFF_1: 15, AFF_1:def 3;

        assume

         A56: LIN (b9,p,q);

        then

         A57: LIN (b9,q,p) by AFF_1: 6;

         A58:

        now

          

           A59: C9 <> M

          proof

            assume C9 = M;

            then LIN (c,c9,b) by A45, A33, A30, A49, AFF_1: 21;

            then b in C by A4, A15, A16, A43, AFF_1: 25;

            hence contradiction by A3, A4, A6, A11, A12, A14, A18, AFF_1: 18;

          end;

          assume b9 <> q;

          then

           A60: p in C9 by A57, A55, A53, AFF_1: 25;

          then LIN (b,a,b9) by A24, A50, A54, A55, A52, AFF_1: 18;

          then b9 in K by AFF_1:def 2;

          then

           A61: b = b9 by A3, A12, A13, A46, A41, A47, AFF_1: 18;

          p = b9 by A50, A54, A55, A52, A60, AFF_1: 18;

          then p = q by A45, A33, A39, A55, A53, A61, A59, AFF_1: 18;

          hence thesis by AFF_1: 3;

        end;

        now

          

           A62: A9 <> K

          proof

            assume A9 = K;

            then LIN (a,a9,b) by A46, A41, A34, A51, AFF_1: 21;

            then b in A by A2, A9, A10, A23, AFF_1: 25;

            hence contradiction by A2, A3, A5, A8, A11, A12, A18, AFF_1: 18;

          end;

          assume b9 <> p;

          then

           A63: q in A9 by A56, A50, A54, AFF_1: 25;

          then LIN (b,c,b9) by A26, A50, A55, A53, A52, AFF_1: 18;

          then b9 in M by AFF_1:def 2;

          then

           A64: b = b9 by A3, A12, A13, A45, A33, A32, AFF_1: 18;

          q = b9 by A50, A55, A53, A52, A63, AFF_1: 18;

          then p = q by A46, A41, A36, A50, A54, A64, A62, AFF_1: 18;

          hence thesis by AFF_1: 3;

        end;

        hence thesis by A20, A58;

      end;

      

       A65: K <> M by A21, A46, A41, A34, A30, AFF_1: 21;

      now

        

         A66: LIN (o,c,c9) & LIN (b9,q,c9) by A4, A14, A15, A16, A27, AFF_1: 6, AFF_1: 21;

        assume

         A67: not LIN (b9,p,q);

         LIN (o,a,a9) & LIN (b9,p,a9) by A2, A8, A9, A10, A25, AFF_1: 6, AFF_1: 21;

        hence thesis by A1, A3, A11, A12, A13, A18, A28, A46, A45, A41, A34, A33, A30, A36, A39, A31, A35, A37, A38, A65, A42, A43, A67, A66;

      end;

      hence thesis by A48;

    end;

    theorem :: AFF_3:3

    AP is Desarguesian implies AP is satisfying_DES1

    proof

      assume

       A1: AP is Desarguesian;

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

      assume that

       A2: A is being_line and

       A3: P is being_line and

       A4: C is being_line and

       A5: P <> A and

       A6: P <> C and

       A7: A <> C and

       A8: o in A and

       A9: a in A and

       A10: a9 in A and

       A11: o in P and

       A12: b in P and

       A13: b9 in P and

       A14: o in C and

       A15: c in C and

       A16: c9 in C and

       A17: o <> a and

       A18: o <> b and

       A19: o <> c and p <> q and

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

       A21: not LIN (b9,a9,c9) and

       A22: a <> a9 and

       A23: LIN (b,a,p) and

       A24: LIN (b9,a9,p) and

       A25: LIN (b,c,q) and

       A26: LIN (b9,c9,q) and

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

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

      b <> c by A20, AFF_1: 7;

      then D is being_line by AFF_1:def 3;

      then

      consider D9 such that

       A28: c9 in D9 and

       A29: D // D9 by AFF_1: 49;

      

       A30: D9 is being_line by A29, AFF_1: 36;

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

      

       A31: q in M by A26, AFF_1:def 2;

      

       A32: b in D by AFF_1: 15;

      

       A33: c in D by AFF_1: 15;

       not D9 // P

      proof

        assume D9 // P;

        then D // P by A29, AFF_1: 44;

        then c in P by A12, A32, A33, AFF_1: 45;

        hence contradiction by A3, A4, A6, A11, A14, A15, A19, AFF_1: 18;

      end;

      then

      consider d such that

       A34: d in D9 and

       A35: d in P by A3, A30, AFF_1: 58;

      

       A36: q in D by A25, AFF_1:def 2;

      then

       A37: (d,c9) // (b,q) by A32, A28, A29, A34, AFF_1: 39;

      

       A38: a <> b & (b,a) // (b,p) by A20, A23, AFF_1: 7, AFF_1:def 1;

      

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

      (c,b) // (c9,d) by A32, A33, A28, A29, A34, AFF_1: 39;

      then (b,a) // (d,a9) by A1, A2, A3, A4, A6, A7, A8, A9, A10, A11, A12, A14, A15, A16, A17, A18, A19, A35, A39;

      then

       A40: (d,a9) // (b,p) by A38, AFF_1: 5;

      set K = ( Line (b9,a9));

      

       A41: b9 in K & p in K by A24, AFF_1: 15, AFF_1:def 2;

      

       A42: a9 <> b9 by A21, AFF_1: 7;

      then

       A43: K is being_line by AFF_1:def 3;

      

       A44: b9 in M by AFF_1: 15;

      

       A45: c9 in M by AFF_1: 15;

      

       A46: b9 <> c9 by A21, AFF_1: 7;

      then

       A47: M is being_line by AFF_1:def 3;

      

       A48: not LIN (o,a,c)

      proof

        assume LIN (o,a,c);

        then c in A by A2, A8, A9, A17, AFF_1: 25;

        hence contradiction by A2, A4, A7, A8, A14, A15, A19, AFF_1: 18;

      end;

      

       A49: c <> c9

      proof

        assume c = c9;

        then

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

         LIN (o,a,a9) & not LIN (o,c,a) by A2, A8, A9, A10, A48, AFF_1: 6, AFF_1: 21;

        hence contradiction by A22, A50, AFF_1: 14;

      end;

      

       A51: d <> b9

      proof

        assume d = b9;

        then M = D9 by A46, A47, A44, A45, A28, A30, A34, AFF_1: 18;

        then D = M by A31, A36, A29, AFF_1: 45;

        then LIN (c,c9,b) by A47, A45, A32, A33, AFF_1: 21;

        then b in C by A4, A15, A16, A49, AFF_1: 25;

        hence contradiction by A3, A4, A6, A11, A12, A14, A18, AFF_1: 18;

      end;

      

       A52: a9 <> c9 by A21, AFF_1: 7;

      

       A53: o <> a9 by A4, A14, A15, A16, A27, A52, A48, AFF_1: 21, AFF_1: 55;

      o <> c9

      proof

        

         A54: not LIN (o,c,a) by A48, AFF_1: 6;

        assume

         A55: o = c9;

         LIN (o,a,a9) & (c,a) // (c9,a9) by A2, A8, A9, A10, A27, AFF_1: 4, AFF_1: 21;

        hence contradiction by A53, A55, A54, AFF_1: 55;

      end;

      then

       A56: M <> P by A3, A4, A6, A11, A14, A16, A45, AFF_1: 18;

      

       A57: a9 in K by AFF_1: 15;

      then K <> P by A2, A3, A5, A8, A10, A11, A53, AFF_1: 18;

      then (a9,c9) // (p,q) by A1, A3, A12, A13, A42, A46, A43, A47, A57, A41, A44, A45, A31, A56, A35, A51, A40, A37;

      hence thesis by A27, A52, AFF_1: 5;

    end;

    theorem :: AFF_3:4

    AP is Desarguesian implies AP is satisfying_DES1_2

    proof

      assume

       A1: AP is Desarguesian;

      then

       A2: AP is satisfying_DES_1 by AFF_2: 2;

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

      assume that

       A3: A is being_line and

       A4: P is being_line and

       A5: C is being_line and

       A6: P <> A and

       A7: P <> C and A <> C and

       A8: o in A and

       A9: a in A & a9 in A and

       A10: o in P and

       A11: b in P and

       A12: b9 in P and

       A13: c in C and

       A14: c9 in C and

       A15: o <> a and

       A16: o <> b and o <> c and

       A17: p <> q and

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

       A19: not LIN (b9,a9,c9) and

       A20: c <> c9 and

       A21: LIN (b,a,p) and

       A22: LIN (b9,a9,p) and

       A23: LIN (b,c,q) and

       A24: LIN (b9,c9,q) and

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

       A26: (a,c) // (p,q);

      

       A27: b <> p by A17, A18, A23, A26, AFF_1: 55;

      set K = ( Line (b9,a9));

      

       A28: p in K by A22, AFF_1:def 2;

      a9 <> b9 by A19, AFF_1: 7;

      then

       A29: K is being_line by AFF_1:def 3;

      

       A30: b <> q

      proof

        assume

         A31: b = q;

        ( not LIN (b,c,a)) & (c,a) // (q,p) by A18, A26, AFF_1: 4, AFF_1: 6;

        hence contradiction by A17, A21, A31, AFF_1: 55;

      end;

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

      

       A32: q in M by A24, AFF_1:def 2;

      

       A33: c9 in M by AFF_1: 15;

      

       A34: a <> c by A18, AFF_1: 7;

      

       A35: b9 <> p

      proof

        assume

         A36: b9 = p;

        (a9,c9) // (p,q) by A25, A26, A34, AFF_1: 5;

        hence contradiction by A17, A19, A24, A36, AFF_1: 55;

      end;

      

       A37: b9 <> q

      proof

        (a9,c9) // (p,q) by A25, A26, A34, AFF_1: 5;

        then

         A38: (c9,a9) // (q,p) by AFF_1: 4;

        assume

         A39: b9 = q;

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

        hence contradiction by A17, A22, A39, A38, AFF_1: 55;

      end;

      

       A40: b <> c by A18, AFF_1: 7;

      

       A41: a <> b by A18, AFF_1: 7;

      

       A42: b9 <> a9 & b9 <> c9 by A19, AFF_1: 7;

      

       A43: a9 in K by AFF_1: 15;

      

       A44: b9 in M by AFF_1: 15;

      

       A45: b9 <> c9 by A19, AFF_1: 7;

      then

       A46: M is being_line by AFF_1:def 3;

      

       A47: b9 in K by AFF_1: 15;

      then

       A48: K <> M by A19, A29, A43, A33, AFF_1: 21;

      now

         A49:

        now

          (p,q) // (a9,c9) by A25, A26, A34, AFF_1: 5;

          then

           A50: (c9,a9) // (q,p) by AFF_1: 4;

          

           A51: (b,a) // (b,p) by A21, AFF_1:def 1;

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

          

           A52: b in D by AFF_1: 15;

          D is being_line by A40, AFF_1:def 3;

          then

          consider D9 such that

           A53: c9 in D9 and

           A54: D // D9 by AFF_1: 49;

          

           A55: D9 is being_line by A54, AFF_1: 36;

          

           A56: q in D by A23, AFF_1:def 2;

          assume

           A57: M <> P;

           not D9 // P

          proof

            assume D9 // P;

            then D // P by A54, AFF_1: 44;

            then q in P by A11, A52, A56, AFF_1: 45;

            hence contradiction by A4, A12, A46, A44, A32, A37, A57, AFF_1: 18;

          end;

          then

          consider d such that

           A58: d in D9 and

           A59: d in P by A4, A55, AFF_1: 58;

          

           A60: c in D by AFF_1: 15;

          

           A61: d <> b9

          proof

            assume d = b9;

            then M = D9 by A45, A46, A44, A33, A53, A55, A58, AFF_1: 18;

            then

             A62: D = M by A32, A56, A54, AFF_1: 45;

            then LIN (c,c9,b) by A46, A33, A52, A60, AFF_1: 21;

            then

             A63: b in C by A5, A13, A14, A20, AFF_1: 25;

            set N = ( Line (a,c));

            set T = ( Line (b,a));

            

             A64: b in T by AFF_1: 15;

            

             A65: c in N by AFF_1: 15;

            

             A66: a in T by AFF_1: 15;

            

             A67: N is being_line by A34, AFF_1:def 3;

            

             A68: a in N by AFF_1: 15;

            

             A69: a <> a9

            proof

              assume a = a9;

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

              then c9 in N by AFF_1:def 2;

              then N = C by A5, A13, A14, A20, A67, A65, AFF_1: 18;

              hence contradiction by A13, A18, A63, A67, A68, AFF_1: 21;

            end;

            

             A70: T is being_line & p in T by A21, A41, AFF_1:def 2, AFF_1:def 3;

            

             A71: b <> b9

            proof

              

               A72: K <> T

              proof

                assume K = T;

                then T = A by A3, A9, A29, A43, A66, A69, AFF_1: 18;

                hence contradiction by A3, A4, A6, A8, A10, A11, A16, A64, AFF_1: 18;

              end;

              assume b = b9;

              hence contradiction by A29, A47, A28, A35, A64, A70, A72, AFF_1: 18;

            end;

             LIN (c,c9,b9) by A46, A44, A33, A60, A62, AFF_1: 21;

            then b9 in C by A5, A13, A14, A20, AFF_1: 25;

            hence contradiction by A4, A5, A7, A11, A12, A63, A71, AFF_1: 18;

          end;

          (c9,d) // (q,b) by A52, A56, A53, A54, A58, AFF_1: 39;

          then (d,a9) // (b,p) by A1, A4, A11, A12, A42, A29, A46, A47, A43, A28, A44, A33, A32, A48, A57, A59, A61, A50;

          then

           A73: (b,a) // (d,a9) by A27, A51, AFF_1: 5;

          (b,c) // (d,c9) by A52, A60, A53, A54, A58, AFF_1: 39;

          hence thesis by A2, A3, A4, A5, A6, A8, A9, A10, A11, A13, A14, A15, A16, A18, A20, A25, A59, A73;

        end;

        now

          assume

           A74: M = P;

           LIN (b,q,c) by A23, AFF_1: 6;

          then c in P by A11, A46, A32, A30, A74, AFF_1: 25;

          then P = ( Line (c,c9)) by A20, A46, A33, A74, AFF_1: 57;

          hence thesis by A5, A10, A13, A14, A20, AFF_1: 57;

        end;

        hence thesis by A49;

      end;

      hence thesis;

    end;

    theorem :: AFF_3:5

    AP is satisfying_DES1_2 implies AP is satisfying_DES1_3

    proof

      assume

       A1: AP is satisfying_DES1_2;

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

      assume that

       A2: A is being_line and

       A3: P is being_line and

       A4: C is being_line and

       A5: P <> A and

       A6: P <> C and

       A7: A <> C and

       A8: o in A and

       A9: a in A and

       A10: a9 in A and

       A11: b in P and

       A12: b9 in P and

       A13: o in C and

       A14: c in C and

       A15: c9 in C and

       A16: o <> a and

       A17: o <> b and

       A18: o <> c and

       A19: p <> q and

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

       A21: not LIN (b9,a9,c9) and

       A22: b <> b9 and

       A23: a <> a9 and

       A24: LIN (b,a,p) and

       A25: LIN (b9,a9,p) and

       A26: LIN (b,c,q) and

       A27: LIN (b9,c9,q) and

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

       A29: (a,c) // (p,q);

      set D = ( Line (b,c)), K = ( Line (b9,a9));

      assume

       A30: not thesis;

      

       A31: not LIN (o,c,a)

      proof

        assume LIN (o,c,a);

        then a in C by A4, A13, A14, A18, AFF_1: 25;

        hence contradiction by A2, A4, A7, A8, A9, A13, A16, AFF_1: 18;

      end;

      

       A32: c <> c9

      proof

        assume c = c9;

        then

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

         LIN (o,a,a9) by A2, A8, A9, A10, AFF_1: 21;

        hence contradiction by A23, A31, A33, AFF_1: 14;

      end;

      a <> c by A20, AFF_1: 7;

      then

       A34: (a9,c9) // (p,q) by A28, A29, AFF_1: 5;

      

       A35: p <> b & p <> b9 & q <> b & q <> b9

      proof

         A36:

        now

          assume

           A37: b9 = q;

          ( not LIN (b9,c9,a9)) & (c9,a9) // (q,p) by A21, A34, AFF_1: 4, AFF_1: 6;

          hence contradiction by A19, A25, A37, AFF_1: 55;

        end;

         A38:

        now

          assume

           A39: b = q;

          ( not LIN (b,c,a)) & (c,a) // (q,p) by A20, A29, AFF_1: 4, AFF_1: 6;

          hence contradiction by A19, A24, A39, AFF_1: 55;

        end;

        assume not thesis;

        hence contradiction by A20, A21, A26, A27, A29, A34, A38, A36, AFF_1: 55;

      end;

      

       A40: b <> c by A20, AFF_1: 7;

      then

       A41: D is being_line & c in D by AFF_1: 24;

      

       A42: b in D by A40, AFF_1: 24;

      then

       A43: q in D by A26, A40, A41, AFF_1: 25;

       A44:

      now

        assume not C // P;

        then

        consider x such that

         A45: x in C and

         A46: x in P by A3, A4, AFF_1: 58;

        

         A47: x <> c

        proof

          

           A48: LIN (q,b9,c9) & LIN (q,b9,b9) by A27, AFF_1: 6, AFF_1: 7;

          assume

           A49: x = c;

          then LIN (b,c,b9) & LIN (b,c,c) by A3, A11, A12, A46, AFF_1: 21;

          then LIN (q,b9,c) by A26, A40, AFF_1: 8;

          then

           A50: b9 in C by A4, A14, A15, A32, A35, A48, AFF_1: 8, AFF_1: 25;

          then LIN (c,c9,q) by A3, A4, A6, A12, A14, A27, A46, A49, AFF_1: 18;

          then

           A51: q in C by A4, A14, A15, A32, AFF_1: 25;

          c = b9 by A3, A4, A6, A12, A14, A46, A49, A50, AFF_1: 18;

          then C = D by A4, A14, A35, A41, A43, A51, AFF_1: 18;

          hence contradiction by A3, A4, A6, A11, A12, A22, A42, A50, AFF_1: 18;

        end;

        

         A52: x <> b

        proof

          

           A53: LIN (q,c9,b9) by A27, AFF_1: 6;

          assume

           A54: x = b;

          then q in C by A4, A14, A26, A40, A45, AFF_1: 25;

          then q = c9 or b9 in C by A4, A15, A53, AFF_1: 25;

          then (c9,a9) // (c9,p) by A3, A4, A6, A11, A12, A22, A34, A45, A54, AFF_1: 4, AFF_1: 18;

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

          then

           A55: LIN (p,a9,c9) by AFF_1: 6;

           LIN (p,a9,b9) & LIN (p,a9,a9) by A25, AFF_1: 6, AFF_1: 7;

          then p = a9 by A21, A55, AFF_1: 8;

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

          then b in A by A2, A9, A10, A23, AFF_1: 25;

          hence contradiction by A2, A4, A7, A8, A13, A17, A45, A54, AFF_1: 18;

        end;

        

         A56: (c,a) // (q,p) & (c,a) // (c9,a9) by A28, A29, AFF_1: 4;

        ( not LIN (b,c,a)) & not LIN (b9,c9,a9) by A20, A21, AFF_1: 6;

        then x in A by A1, A2, A3, A4, A6, A9, A10, A11, A12, A14, A15, A19, A23, A24, A25, A26, A27, A45, A46, A47, A52, A56;

        hence contradiction by A2, A4, A7, A8, A13, A30, A45, A46, AFF_1: 18;

      end;

      

       A57: a <> b by A20, AFF_1: 7;

      

       A58: a9 <> b9 by A21, AFF_1: 7;

      then

       A59: a9 in K by AFF_1: 24;

      

       A60: K is being_line & b9 in K by A58, AFF_1: 24;

      then

       A61: p in K by A25, A58, A59, AFF_1: 25;

       A62:

      now

        assume not P // A;

        then

        consider x such that

         A63: x in P and

         A64: x in A by A2, A3, AFF_1: 58;

        

         A65: x <> b

        proof

          assume

           A66: x = b;

          then p in A by A2, A9, A24, A57, A64, AFF_1: 25;

          then (a9,c9) // (a9,q) or b9 in A by A2, A10, A34, A60, A59, A61, AFF_1: 18;

          then LIN (a9,c9,q) by A2, A3, A5, A11, A12, A22, A64, A66, AFF_1: 18, AFF_1:def 1;

          then

           A67: LIN (q,c9,a9) by AFF_1: 6;

           LIN (q,c9,b9) & LIN (q,c9,c9) by A27, AFF_1: 6, AFF_1: 7;

          then q = c9 by A21, A67, AFF_1: 8;

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

          then b in C by A4, A14, A15, A32, AFF_1: 25;

          hence contradiction by A2, A4, A7, A8, A13, A17, A64, A66, AFF_1: 18;

        end;

        x <> a

        proof

          assume x = a;

          then p in P & K <> P by A2, A3, A5, A9, A10, A11, A23, A24, A57, A59, A63, AFF_1: 18, AFF_1: 25;

          hence contradiction by A3, A12, A35, A60, A61, AFF_1: 18;

        end;

        then x in C by A1, A2, A3, A4, A5, A9, A10, A11, A12, A14, A15, A19, A20, A21, A24, A25, A26, A27, A28, A29, A32, A63, A64, A65;

        hence contradiction by A2, A4, A7, A8, A13, A30, A63, A64, AFF_1: 18;

      end;

       not P // A or not C // P

      proof

        assume not thesis;

        then C // A by AFF_1: 44;

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

      end;

      hence contradiction by A62, A44;

    end;

    theorem :: AFF_3:6

    AP is satisfying_DES1_2 implies AP is Desarguesian

    proof

      assume

       A1: AP is satisfying_DES1_2;

      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 in C and

       A5: o <> a and

       A6: o <> b and

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

      now

        

         A21: not LIN (o,b,a) & not LIN (o,a,c)

        proof

           A22:

          now

            assume LIN (o,a,c);

            then c in A by A2, A5, A8, A14, AFF_1: 25;

            hence contradiction by A2, A4, A7, A12, A14, A16, A18, AFF_1: 18;

          end;

           A23:

          now

            assume LIN (o,b,a);

            then a in P by A3, A6, A10, A15, AFF_1: 25;

            hence contradiction by A2, A3, A5, A8, A14, A15, A17, AFF_1: 18;

          end;

          assume not thesis;

          hence thesis by A23, A22;

        end;

        

         A24: b = b9 implies thesis

        proof

          

           A25: LIN (o,c,c9) by A4, A12, A13, A16, AFF_1: 21;

          

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

          assume

           A27: b = b9;

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

          then (a,c) // (a,c9) by A20, A21, A26, AFF_1: 14;

          then c = c9 by A21, A25, AFF_1: 14;

          hence thesis by A27, AFF_1: 2;

        end;

        

         A28: a9 = o implies thesis

        proof

          assume

           A29: a9 = o;

           LIN (o,b,b9) & not LIN (o,a,b) by A3, A10, A11, A15, A21, AFF_1: 6, AFF_1: 21;

          then

           A30: o = b9 by A19, A29, AFF_1: 55;

           LIN (o,c,c9) by A4, A12, A13, A16, AFF_1: 21;

          then o = c9 by A20, A21, A29, AFF_1: 55;

          hence thesis by A30, AFF_1: 3;

        end;

        

         A31: c9 = o implies thesis

        proof

          

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

          assume

           A33: c9 = o;

           LIN (o,a,a9) & not LIN (o,c,a) by A2, A8, A9, A14, A21, AFF_1: 6, AFF_1: 21;

          hence thesis by A28, A33, A32, AFF_1: 55;

        end;

        set K = ( Line (a,c));

        

         A34: a in K by AFF_1: 15;

        

         A35: a <> c by A2, A4, A5, A8, A12, A14, A16, A18, AFF_1: 18;

        then

         A36: K is being_line by AFF_1:def 3;

        

         A37: c in K by AFF_1: 15;

        

         A38: a <> b by A2, A3, A5, A8, A10, A14, A15, A17, AFF_1: 18;

        

         A39: LIN (a,b,c) implies thesis

        proof

          consider N such that

           A40: a9 in N and

           A41: K // N by A36, AFF_1: 49;

          

           A42: N is being_line by A41, AFF_1: 36;

          (a9,c9) // K by A20, A35, AFF_1: 29, AFF_1: 32;

          then (a9,c9) // N by A41, AFF_1: 43;

          then

           A43: c9 in N by A40, A42, AFF_1: 23;

          assume LIN (a,b,c);

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

          then

           A44: b in K by AFF_1:def 2;

          then K = ( Line (a,b)) by A38, A36, A34, AFF_1: 57;

          then (a9,b9) // K by A19, A38, AFF_1: 29, AFF_1: 32;

          then (a9,b9) // N by A41, AFF_1: 43;

          then b9 in N by A40, A42, AFF_1: 23;

          hence thesis by A37, A44, A41, A43, AFF_1: 39;

        end;

        assume

         A45: P <> C;

         A46:

        now

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

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

          set N = ( Line (a9,c9));

          assume that

           A47: o <> a9 and

           A48: o <> b9 and

           A49: o <> c9 and

           A50: b <> b9 and

           A51: not LIN (a,b,c);

          

           A52: c9 in N by AFF_1: 15;

          assume not (b,c) // (b9,c9);

          then

          consider q such that

           A53: LIN (b,c,q) and

           A54: LIN (b9,c9,q) by AFF_1: 60;

          consider M such that

           A55: q in M and

           A56: K // M by A36, AFF_1: 49;

          

           A57: M is being_line by A56, AFF_1: 36;

           not (a,b) // M

          proof

            assume (a,b) // M;

            then (a,b) // K by A56, AFF_1: 43;

            then b in K by A36, A34, AFF_1: 23;

            hence contradiction by A36, A34, A37, A51, AFF_1: 21;

          end;

          then

          consider p such that

           A58: p in M and

           A59: LIN (a,b,p) by A57, AFF_1: 59;

          

           A60: a9 in N by AFF_1: 15;

          

           A61: p <> q

          proof

            

             A62: LIN (p,b,a) & LIN (p,b,b) by A59, AFF_1: 6, AFF_1: 7;

            assume

             A63: p = q;

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

            then p = b by A51, A62, AFF_1: 8;

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

            then c9 in P by A10, A11, A15, A50, AFF_1: 25;

            hence contradiction by A3, A4, A13, A15, A16, A45, A49, AFF_1: 18;

          end;

          

           A64: (c,a) // (q,p) by A34, A37, A55, A56, A58, AFF_1: 39;

          

           A65: LIN (b,a,p) by A59, AFF_1: 6;

          

           A66: b9 <> c9 by A3, A4, A11, A13, A15, A16, A45, A48, AFF_1: 18;

          

           A67: a9 <> c9 by A2, A4, A9, A13, A14, A16, A18, A47, AFF_1: 18;

          then

           A68: N is being_line by AFF_1:def 3;

          

           A69: K // N by A20, A35, A67, AFF_1: 37;

          then

           A70: N // M by A56, AFF_1: 44;

          

           A71: a9 <> b9 by A2, A3, A9, A11, A14, A15, A17, A47, AFF_1: 18;

          

           A72: not LIN (a9,b9,c9)

          proof

            assume LIN (a9,b9,c9);

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

            then b9 in N by AFF_1:def 2;

            then (a9,b9) // N by A68, A60, AFF_1: 23;

            then

             A73: (a9,b9) // K by A69, AFF_1: 43;

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

            then (a,b) // K by A71, A73, AFF_1: 32;

            then b in K by A36, A34, AFF_1: 23;

            hence contradiction by A36, A34, A37, A51, AFF_1: 21;

          end;

           not (b9,p) // N

          proof

            assume (b9,p) // N;

            then (b9,p) // M by A70, AFF_1: 43;

            then (p,b9) // M by AFF_1: 34;

            then

             A74: b9 in M by A57, A58, AFF_1: 23;

             A75:

            now

              assume

               A76: b9 <> q;

               LIN (b9,q,c9) by A54, AFF_1: 6;

              then c9 in M by A55, A57, A74, A76, AFF_1: 25;

              then a9 in N & b9 in N by A52, A70, A74, AFF_1: 15, AFF_1: 45;

              hence contradiction by A68, A52, A72, AFF_1: 21;

            end;

            now

              assume b9 = q;

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

              then c in P by A10, A11, A15, A50, AFF_1: 25;

              hence contradiction by A3, A4, A7, A12, A15, A16, A45, AFF_1: 18;

            end;

            hence thesis by A75;

          end;

          then

          consider x such that

           A77: x in N and

           A78: LIN (b9,p,x) by A68, AFF_1: 59;

          set A9 = ( Line (x,a));

          

           A79: a <> a9

          proof

            assume

             A80: a = a9;

            ( not LIN (o,a,b)) & LIN (o,b,b9) by A3, A10, A11, A15, A21, AFF_1: 6, AFF_1: 21;

            hence contradiction by A19, A50, A80, AFF_1: 14;

          end;

          

           A81: x <> a

          proof

            assume x = a;

            then a9 in K by A34, A60, A69, A77, AFF_1: 45;

            then A = K by A8, A9, A14, A36, A34, A79, AFF_1: 18;

            hence contradiction by A2, A4, A7, A12, A14, A16, A18, A37, AFF_1: 18;

          end;

          then

           A82: A9 is being_line by AFF_1:def 3;

          

           A83: c <> c9

          proof

            assume c = c9;

            then

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

            ( not LIN (o,c,a)) & LIN (o,a,a9) by A2, A8, A9, A14, A21, AFF_1: 6, AFF_1: 21;

            hence contradiction by A79, A84, AFF_1: 14;

          end;

          

           A85: not LIN (b9,c9,x)

          proof

             A86:

            now

               A87:

              now

                assume q = c9;

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

                then b in C by A12, A13, A16, A83, AFF_1: 25;

                hence contradiction by A3, A4, A6, A10, A15, A16, A45, AFF_1: 18;

              end;

              assume c9 = x;

              then

               A88: LIN (b9,c9,p) by A78, AFF_1: 6;

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

              then c9 in M by A66, A54, A55, A57, A58, A61, A88, AFF_1: 8, AFF_1: 25;

              then

               A89: q in N by A55, A52, A70, AFF_1: 45;

               LIN (q,c9,b9) by A54, AFF_1: 6;

              then q = c9 or b9 in N by A68, A52, A89, AFF_1: 25;

              hence LIN (b9,c9,a9) by A68, A60, A52, A87, AFF_1: 21;

            end;

            assume LIN (b9,c9,x);

            then

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

            

             A91: LIN (c9,x,a9) & LIN (c9,x,c9) by A68, A60, A52, A77, AFF_1: 21;

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

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

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

            then

             A92: (a,c) // (b9,c9) by A20, A67, AFF_1: 5;

            c9 = x or LIN (b9,c9,a9) by A90, A91, AFF_1: 8;

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

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

            then (b9,c9) // (a,b) by A19, A71, AFF_1: 5;

            then (a,c) // (a,b) by A66, A92, AFF_1: 5;

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

            hence contradiction by A51, AFF_1: 6;

          end;

          

           A93: x in A9 & a in A9 by AFF_1: 15;

          A <> K by A2, A4, A7, A12, A14, A16, A18, A37, AFF_1: 18;

          then

           A94: A <> N by A8, A34, A69, AFF_1: 45;

          

           A95: not LIN (b,c,a) by A51, AFF_1: 6;

          

           A96: p in D by A59, AFF_1:def 2;

          

           A97: D is being_line & b in D by A38, AFF_1: 15, AFF_1:def 3;

          

           A98: LIN (b9,x,p) by A78, AFF_1: 6;

          (c,a) // (c9,x) by A34, A37, A52, A69, A77, AFF_1: 39;

          then o in A9 by A1, A3, A4, A6, A7, A10, A11, A12, A13, A15, A16, A45, A53, A54, A98, A81, A82, A93, A61, A85, A64, A95, A65;

          then x in A by A2, A5, A8, A14, A82, A93, AFF_1: 18;

          then x = a9 by A9, A14, A68, A60, A77, A94, AFF_1: 18;

          then

           A99: a9 in T & p in T by A98, AFF_1: 15, AFF_1:def 2;

          D // T by A19, A38, A71, AFF_1: 37;

          then a in D & a9 in D by A96, A99, AFF_1: 15, AFF_1: 45;

          then b in A by A8, A9, A14, A79, A97, AFF_1: 18;

          hence contradiction by A2, A3, A6, A10, A14, A15, A17, AFF_1: 18;

        end;

        b9 = o implies thesis

        proof

          assume

           A100: b9 = o;

           LIN (o,a,a9) & (b,a) // (b9,a9) by A2, A8, A9, A14, A19, AFF_1: 4, AFF_1: 21;

          hence thesis by A21, A28, A100, AFF_1: 55;

        end;

        hence thesis by A28, A31, A39, A24, A46;

      end;

      hence thesis by A10, A11, A12, A13, A15, AFF_1: 51;

    end;

    theorem :: AFF_3:7

    AP is satisfying_DES2_1 implies AP is satisfying_DES2

    proof

      assume

       A1: AP is satisfying_DES2_1;

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

      assume that

       A2: A is being_line and

       A3: P is being_line and

       A4: C is being_line and

       A5: A <> P and

       A6: A <> C and

       A7: P <> 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 // P and

       A15: A // C and

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

       A17: not LIN (b9,a9,c9) and

       A18: p <> q and

       A19: a <> a9 and

       A20: LIN (b,a,p) and

       A21: LIN (b9,a9,p) and

       A22: LIN (b,c,q) & LIN (b9,c9,q) and

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

      

       A24: P // C by A14, A15, AFF_1: 44;

      set P9 = ( Line (b9,a9));

      

       A25: p in P9 by A21, AFF_1:def 2;

      a9 <> b9 by A17, AFF_1: 7;

      then

       A26: P9 is being_line by AFF_1:def 3;

      set K = ( Line (a,c)), N = ( Line (a9,c9)), D = ( Line (b,c)), T = ( Line (b9,c9));

      

       A27: q in D & q in T by A22, AFF_1:def 2;

      

       A28: c9 in N by AFF_1: 15;

      b <> c by A16, AFF_1: 7;

      then

       A29: D is being_line by AFF_1:def 3;

      b9 <> c9 by A17, AFF_1: 7;

      then

       A30: T is being_line by AFF_1:def 3;

      

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

      then

       A32: K is being_line by AFF_1:def 3;

      

       A33: a9 <> c9 by A17, AFF_1: 7;

      then

       A34: N is being_line by AFF_1:def 3;

      then

      consider M such that

       A35: p in M and

       A36: N // M by AFF_1: 49;

      

       A37: K // N by A23, A31, A33, AFF_1: 37;

      then

       A38: K // M by A36, AFF_1: 44;

      

       A39: c in D by AFF_1: 15;

      

       A40: b in D by AFF_1: 15;

      set A9 = ( Line (b,a));

      

       A41: p in A9 by A20, AFF_1:def 2;

      a <> b by A16, AFF_1: 7;

      then

       A42: A9 is being_line by AFF_1:def 3;

      

       A43: c9 in T by AFF_1: 15;

      

       A44: b9 in T by AFF_1: 15;

      

       A45: a9 in N by AFF_1: 15;

      

       A46: a in K by AFF_1: 15;

      

       A47: a9 in P9 by AFF_1: 15;

      

       A48: b9 in P9 by AFF_1: 15;

      

       A49: a in A9 by AFF_1: 15;

      

       A50: b in A9 by AFF_1: 15;

      

       A51: c in K by AFF_1: 15;

      then

       A52: K <> A by A6, A12, A15, AFF_1: 45;

      

       A53: c <> c9

      proof

        assume c = c9;

        then K = N by A51, A28, A37, AFF_1: 45;

        hence contradiction by A2, A8, A9, A19, A32, A46, A45, A52, AFF_1: 18;

      end;

      

       A54: D <> T

      proof

        assume D = T;

        then D = C by A4, A12, A13, A29, A39, A43, A53, AFF_1: 18;

        hence contradiction by A7, A10, A24, A40, AFF_1: 45;

      end;

      

       A55: b <> b9

      proof

        

         A56: A9 <> P9

        proof

          assume A9 = P9;

          then A9 = A by A2, A8, A9, A19, A42, A49, A47, AFF_1: 18;

          hence contradiction by A5, A10, A14, A50, AFF_1: 45;

        end;

        assume

         A57: b = b9;

        then b9 = q by A29, A30, A40, A44, A27, A54, AFF_1: 18;

        hence contradiction by A18, A42, A26, A50, A41, A48, A25, A57, A56, AFF_1: 18;

      end;

      

       A58: M is being_line by A36, AFF_1: 36;

       A59:

      now

        assume not T // M;

        then

        consider x such that

         A60: x in T and

         A61: x in M by A30, A58, AFF_1: 58;

        

         A62: p <> x

        proof

          assume p = x;

          then p = b9 or T = P9 by A30, A44, A26, A48, A25, A60, AFF_1: 18;

          then LIN (b,b9,a) or c9 in P9 by A42, A50, A49, A41, AFF_1: 15, AFF_1: 21;

          then a in P by A3, A10, A11, A17, A55, AFF_1: 25, AFF_1:def 2;

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

        end;

         not (b,x) // C

        proof

          assume

           A63: (b,x) // C;

          C // P by A14, A15, AFF_1: 44;

          then (b,x) // P by A63, AFF_1: 43;

          then x in P by A3, A10, AFF_1: 23;

          then b9 in M or c9 in P by A3, A11, A30, A44, A43, A60, A61, AFF_1: 18;

          then b9 = p or M = P9 by A7, A13, A24, A26, A48, A25, A35, A58, AFF_1: 18, AFF_1: 45;

          then LIN (b,b9,a) or N // P9 by A20, A36, AFF_1: 6;

          then a in P or N = P9 by A3, A10, A11, A45, A47, A55, AFF_1: 25, AFF_1: 45;

          hence contradiction by A5, A8, A14, A17, A28, AFF_1: 45, AFF_1:def 2;

        end;

        then

        consider y such that

         A64: y in C and

         A65: LIN (b,x,y) by A4, AFF_1: 59;

        

         A66: LIN (b,y,x) by A65, AFF_1: 6;

        

         A67: not LIN (b,a,y)

        proof

           A68:

          now

            assume x = p;

            then p = b9 or T = P9 by A30, A44, A26, A48, A25, A60, AFF_1: 18;

            then LIN (b,b9,a) or c9 in P9 by A42, A50, A49, A41, AFF_1: 15, AFF_1: 21;

            then a in P by A3, A10, A11, A17, A55, AFF_1: 25, AFF_1:def 2;

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

          end;

          assume LIN (b,a,y);

          then

           A69: LIN (b,y,a) by AFF_1: 6;

           LIN (b,y,b) by AFF_1: 7;

          then b = y or LIN (a,b,x) by A66, A69, AFF_1: 8;

          then x in A9 by A7, A10, A24, A64, AFF_1: 45, AFF_1:def 2;

          then x = p or A9 = M by A42, A41, A35, A58, A61, AFF_1: 18;

          then K = A9 by A46, A49, A38, A68, AFF_1: 45;

          hence contradiction by A16, A51, AFF_1:def 2;

        end;

         LIN (b9,c9,x) & (a9,c9) // (p,x) by A30, A45, A28, A44, A43, A35, A36, A60, A61, AFF_1: 21, AFF_1: 39;

        then (a9,c9) // (a,y) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A13, A14, A15, A17, A20, A21, A64, A66, A67, A62;

        then (a,c) // (a,y) by A23, A33, AFF_1: 5;

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

        then y in K by AFF_1:def 2;

        then K = C or y = c by A4, A12, A32, A51, A64, AFF_1: 18;

        then a in C or LIN (b,c,x) by A65, AFF_1: 6, AFF_1: 15;

        then x in D by A6, A8, A15, AFF_1: 45, AFF_1:def 2;

        then q in M or c9 in D by A29, A30, A43, A27, A60, A61, AFF_1: 18;

        then (a,c) // (p,q) or LIN (c,c9,b) by A29, A46, A51, A40, A39, A35, A38, AFF_1: 21, AFF_1: 39;

        then (a,c) // (p,q) or b in C by A4, A12, A13, A53, AFF_1: 25;

        hence thesis by A7, A10, A24, AFF_1: 45;

      end;

       A70:

      now

        assume not M // D;

        then

        consider x such that

         A71: x in M and

         A72: x in D by A29, A58, AFF_1: 58;

        

         A73: p <> x

        proof

          assume p = x;

          then p = b or D = A9 by A29, A40, A42, A50, A41, A72, AFF_1: 18;

          then LIN (b,b9,a9) or c in A9 by A26, A48, A47, A25, AFF_1: 15, AFF_1: 21;

          then a9 in P by A3, A10, A11, A16, A55, AFF_1: 25, AFF_1:def 2;

          hence contradiction by A5, A9, A14, AFF_1: 45;

        end;

         not (b9,x) // C

        proof

           A74:

          now

            assume b = p;

            then LIN (b,b9,a9) by A26, A48, A47, A25, AFF_1: 21;

            then a9 in P by A3, A10, A11, A55, AFF_1: 25;

            hence contradiction by A5, A9, A14, AFF_1: 45;

          end;

          assume

           A75: (b9,x) // C;

          C // P by A14, A15, AFF_1: 44;

          then (b9,x) // P by A75, AFF_1: 43;

          then x in P by A3, A11, AFF_1: 23;

          then x = b or D = P by A3, A10, A29, A40, A72, AFF_1: 18;

          then b = p or M = A9 by A7, A12, A24, A39, A42, A50, A41, A35, A58, A71, AFF_1: 18, AFF_1: 45;

          then b in K by A46, A50, A49, A38, A74, AFF_1: 45;

          hence contradiction by A16, A32, A46, A51, AFF_1: 21;

        end;

        then

        consider y such that

         A76: y in C and

         A77: LIN (b9,x,y) by A4, AFF_1: 59;

        

         A78: LIN (b9,y,x) by A77, AFF_1: 6;

        

         A79: not LIN (b9,a9,y)

        proof

           A80:

          now

            assume x = p;

            then p = b or D = A9 by A29, A40, A42, A50, A41, A72, AFF_1: 18;

            then LIN (b,b9,a9) or c in A9 by A26, A48, A47, A25, AFF_1: 15, AFF_1: 21;

            then a9 in P by A3, A10, A11, A16, A55, AFF_1: 25, AFF_1:def 2;

            hence contradiction by A5, A9, A14, AFF_1: 45;

          end;

          assume LIN (b9,a9,y);

          then

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

           LIN (b9,y,b9) by AFF_1: 7;

          then b9 = y or LIN (a9,b9,x) by A78, A81, AFF_1: 8;

          then x in P9 by A7, A11, A24, A76, AFF_1: 45, AFF_1:def 2;

          then x = p or P9 = M by A26, A25, A35, A58, A71, AFF_1: 18;

          then N = P9 by A45, A47, A36, A80, AFF_1: 45;

          hence contradiction by A17, A28, AFF_1:def 2;

        end;

         LIN (b,c,x) & (a,c) // (p,x) by A29, A46, A51, A40, A39, A35, A38, A71, A72, AFF_1: 21, AFF_1: 39;

        then (a,c) // (a9,y) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A14, A15, A16, A20, A21, A76, A78, A79, A73;

        then (a9,y) // (a9,c9) by A23, A31, AFF_1: 5;

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

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

        then y in N by AFF_1:def 2;

        then N = C or y = c9 by A4, A13, A34, A28, A76, AFF_1: 18;

        then a9 in C or LIN (b9,c9,x) by A77, AFF_1: 6, AFF_1: 15;

        then x in T by A6, A9, A15, AFF_1: 45, AFF_1:def 2;

        then q in M or c9 in D by A29, A30, A43, A27, A71, A72, AFF_1: 18;

        then (a,c) // (p,q) or LIN (c,c9,b) by A29, A46, A51, A40, A39, A35, A38, AFF_1: 21, AFF_1: 39;

        then (a,c) // (p,q) or b in C by A4, A12, A13, A53, AFF_1: 25;

        hence thesis by A7, A10, A24, AFF_1: 45;

      end;

       not M // D or not T // M

      proof

        assume not thesis;

        then T // D by AFF_1: 44;

        hence contradiction by A27, A54, AFF_1: 45;

      end;

      hence thesis by A70, A59;

    end;

    theorem :: AFF_3:8

    AP is satisfying_DES2_1 iff AP is satisfying_DES2_3

    proof

      

       A1: AP is satisfying_DES2_1 implies AP is satisfying_DES2_3

      proof

        assume

         A2: AP is satisfying_DES2_1;

        thus AP is satisfying_DES2_3

        proof

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

          assume that

           A3: A is being_line and

           A4: P is being_line and

           A5: C is being_line and

           A6: A <> P and

           A7: A <> C and

           A8: P <> C and

           A9: a in A and

           A10: a9 in A and

           A11: b in P and

           A12: b9 in P and

           A13: c in C and

           A14: c9 in C and

           A15: A // P and

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

           A17: not LIN (b9,a9,c9) and

           A18: p <> q and

           A19: c <> c9 and

           A20: LIN (b,a,p) and

           A21: LIN (b9,a9,p) and

           A22: LIN (b,c,q) and

           A23: LIN (b9,c9,q) and

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

           A25: (a,c) // (p,q);

          now

            set A9 = ( Line (a,c)), P9 = ( Line (p,q)), C9 = ( Line (a9,c9));

            

             A26: LIN (p,a9,b9) by A21, AFF_1: 6;

            

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

            then

             A28: A9 is being_line & a in A9 by AFF_1: 24;

            

             A29: q <> c

            proof

              assume

               A30: q = c;

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

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

              then

               A31: LIN (p,a,c) by AFF_1: 6;

               LIN (p,a,b) & LIN (p,a,a) by A20, AFF_1: 6, AFF_1: 7;

              then a = p by A16, A31, AFF_1: 8;

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

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

              then (a9,c9) // (a9,c) by A6, A12, A15, A24, AFF_1: 4, AFF_1: 45;

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

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

              then

               A32: a9 in C by A5, A13, A14, A19, AFF_1: 25;

               LIN (c,c9,b9) by A23, A30, AFF_1: 6;

              then b9 in C by A5, A13, A14, A19, AFF_1: 25;

              hence contradiction by A5, A14, A17, A32, AFF_1: 21;

            end;

            

             A33: a <> p

            proof

              assume a = p;

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

              then

               A34: LIN (c,q,a) by AFF_1: 6;

               LIN (c,q,b) & LIN (c,q,c) by A22, AFF_1: 6, AFF_1: 7;

              hence contradiction by A16, A29, A34, AFF_1: 8;

            end;

            

             A35: a <> a9

            proof

              

               A36: LIN (p,a,b) & LIN (p,a,a) by A20, AFF_1: 6, AFF_1: 7;

              assume

               A37: a = a9;

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

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

              then

               A38: a in C by A5, A13, A14, A19, AFF_1: 25;

               LIN (p,a,b9) by A21, A37, AFF_1: 6;

              then b = b9 or a in P by A4, A11, A12, A33, A36, AFF_1: 8, AFF_1: 25;

              then

               A39: LIN (q,b,c9) by A6, A9, A15, A23, AFF_1: 6, AFF_1: 45;

               LIN (q,b,c) & LIN (q,b,b) by A22, AFF_1: 6, AFF_1: 7;

              then

               A40: q = b or LIN (c,c9,b) by A39, AFF_1: 8;

               not b in C by A5, A13, A16, A38, AFF_1: 21;

              then LIN (p,q,a) by A5, A13, A14, A19, A20, A40, AFF_1: 6, AFF_1: 25;

              then (p,q) // (p,a) by AFF_1:def 1;

              then (a,c) // (p,a) by A18, A25, AFF_1: 5;

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

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

              then

               A41: p in C by A5, A13, A27, A38, AFF_1: 25;

               LIN (p,a,b) by A20, AFF_1: 6;

              then b in C by A5, A33, A38, A41, AFF_1: 25;

              hence contradiction by A5, A13, A16, A38, AFF_1: 21;

            end;

            

             A42: b <> b9

            proof

              

               A43: (p,q) // (c,a) by A25, AFF_1: 4;

              

               A44: LIN (q,b,c) & LIN (q,b,b) by A22, AFF_1: 6, AFF_1: 7;

              

               A45: LIN (p,b,a) & LIN (p,b,b) by A20, AFF_1: 6, AFF_1: 7;

              assume

               A46: b = b9;

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

              then

               A47: p = b or b in A by A3, A9, A10, A35, A45, AFF_1: 8, AFF_1: 25;

               LIN (q,b,c9) by A23, A46, AFF_1: 6;

              then b = q or LIN (c,c9,b) by A44, AFF_1: 8;

              then

               A48: b in C by A5, A6, A11, A13, A14, A15, A18, A19, A47, AFF_1: 25, AFF_1: 45;

              then q in C by A5, A6, A11, A13, A15, A16, A20, A22, A47, AFF_1: 25, AFF_1: 45;

              then a in C by A5, A6, A11, A13, A15, A18, A47, A48, A43, AFF_1: 45, AFF_1: 48;

              hence contradiction by A5, A13, A16, A48, AFF_1: 21;

            end;

            then

             A49: (a9,a) // (b9,b) by A3, A4, A9, A10, A11, A12, A15, A35, AFF_1: 38;

            

             A50: a9 <> c9 by A17, AFF_1: 7;

            then

             A51: C9 is being_line by AFF_1: 24;

            

             A52: c9 in C9 by A50, AFF_1: 24;

            

             A53: LIN (p,a,b) by A20, AFF_1: 6;

            

             A54: not LIN (p,a9,a)

            proof

              assume LIN (p,a9,a);

              then

               A55: LIN (p,a,a9) by AFF_1: 6;

               LIN (p,a,a) by AFF_1: 7;

              then b in A by A3, A9, A10, A33, A35, A53, A55, AFF_1: 8, AFF_1: 25;

              hence contradiction by A6, A11, A15, AFF_1: 45;

            end;

            

             A56: LIN (q,c9,b9) by A23, AFF_1: 6;

            

             A57: a9 in C9 by A50, AFF_1: 24;

            

             A58: c in A9 by A27, AFF_1: 24;

            then

             A59: C9 // A9 by A24, A27, A50, A51, A28, A57, A52, AFF_1: 38;

            

             A60: A9 <> C9

            proof

              assume

               A61: A9 = C9;

              then LIN (a,a9,c9) by A28, A57, A52, AFF_1: 21;

              then

               A62: c9 in A by A3, A9, A10, A35, AFF_1: 25;

               LIN (a,a9,c) by A28, A58, A57, A61, AFF_1: 21;

              then c in A by A3, A9, A10, A35, AFF_1: 25;

              hence contradiction by A3, A5, A7, A13, A14, A19, A62, AFF_1: 18;

            end;

            

             A63: LIN (q,c,b) by A22, AFF_1: 6;

            

             A64: p in P9 by A18, AFF_1: 24;

            

             A65: A9 <> P9

            proof

              assume A9 = P9;

              then

               A66: LIN (p,a,c) & LIN (p,a,a) by A28, A58, A64, AFF_1: 21;

               LIN (p,a,b) by A20, AFF_1: 6;

              hence contradiction by A16, A33, A66, AFF_1: 8;

            end;

            

             A67: P9 is being_line by A18, AFF_1: 24;

            

             A68: P9 <> C9

            proof

              assume P9 = C9;

              then

               A69: LIN (p,a9,c9) & LIN (p,a9,a9) by A67, A64, A57, A52, AFF_1: 21;

               LIN (p,a9,b9) by A21, AFF_1: 6;

              then p = a9 by A17, A69, AFF_1: 8;

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

              then b in A by A3, A9, A10, A35, AFF_1: 25;

              hence contradiction by A6, A11, A15, AFF_1: 45;

            end;

            

             A70: (a9,c9) // (p,q) by A24, A25, A27, AFF_1: 5;

            

             A71: not LIN (q,c9,c)

            proof

               A72:

              now

                assume q = c9;

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

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

                then p in C9 by A50, A51, A57, A52, AFF_1: 25;

                then p = a9 or b9 in C9 by A51, A57, A26, AFF_1: 25;

                then LIN (a,a9,b) by A17, A20, A51, A57, A52, AFF_1: 6, AFF_1: 21;

                then b in A by A3, A9, A10, A35, AFF_1: 25;

                hence contradiction by A6, A11, A15, AFF_1: 45;

              end;

              assume

               A73: LIN (q,c9,c);

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

              then

               A74: b9 in C by A5, A13, A14, A19, A56, A73, A72, AFF_1: 8, AFF_1: 25;

              

               A75: LIN (q,c,c) by AFF_1: 7;

               LIN (q,c,c9) by A73, AFF_1: 6;

              then b in C by A5, A13, A14, A19, A29, A63, A75, AFF_1: 8, AFF_1: 25;

              hence contradiction by A4, A5, A8, A11, A12, A42, A74, AFF_1: 18;

            end;

            

             A76: q in P9 by A18, AFF_1: 24;

            then C9 // P9 by A18, A50, A67, A51, A64, A57, A52, A70, AFF_1: 38;

            then (a9,a) // (c9,c) by A2, A67, A51, A28, A58, A64, A76, A57, A52, A42, A65, A60, A68, A59, A49, A53, A26, A63, A56, A54, A71;

            hence thesis by A3, A5, A9, A10, A13, A14, A19, A35, AFF_1: 38;

          end;

          hence thesis;

        end;

      end;

      AP is satisfying_DES2_3 implies AP is satisfying_DES2_1

      proof

        assume

         A77: AP is satisfying_DES2_3;

        thus AP is satisfying_DES2_1

        proof

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

          assume that

           A78: A is being_line and

           A79: P is being_line and

           A80: C is being_line and

           A81: A <> P and A <> C and

           A82: P <> C and

           A83: a in A and

           A84: a9 in A and

           A85: b in P and

           A86: b9 in P and

           A87: c in C and

           A88: c9 in C and

           A89: A // P and

           A90: A // C and

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

           A92: not LIN (b9,a9,c9) and

           A93: p <> q and

           A94: LIN (b,a,p) and

           A95: LIN (b9,a9,p) and

           A96: LIN (b,c,q) and

           A97: LIN (b9,c9,q) and

           A98: (a,c) // (p,q);

          

           A99: C // P by A89, A90, AFF_1: 44;

          then

           A100: (c,c9) // (b,b9) by A85, A86, A87, A88, AFF_1: 39;

          assume

           A101: not thesis;

          

           A102: q <> c

          proof

            assume

             A103: q = c;

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

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

            then

             A104: LIN (p,a,c) by AFF_1: 6;

             LIN (p,a,b) & LIN (p,a,a) by A94, AFF_1: 6, AFF_1: 7;

            then a = p by A91, A104, AFF_1: 8;

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

            then

             A105: b9 in A or a = a9 by A78, A83, A84, AFF_1: 25;

             LIN (c,c9,b9) by A97, A103, AFF_1: 6;

            then c = c9 or b9 in C by A80, A87, A88, AFF_1: 25;

            hence contradiction by A81, A82, A86, A89, A101, A99, A105, AFF_1: 2, AFF_1: 45;

          end;

          

           A106: a <> p

          proof

            assume a = p;

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

            then

             A107: LIN (c,q,a) by AFF_1: 6;

             LIN (c,q,b) & LIN (c,q,c) by A96, AFF_1: 6, AFF_1: 7;

            hence contradiction by A91, A102, A107, AFF_1: 8;

          end;

          

           A108: a <> a9

          proof

            

             A109: LIN (p,a,b) & LIN (p,a,a) by A94, AFF_1: 6, AFF_1: 7;

            assume

             A110: a = a9;

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

            then a in P or b = b9 by A79, A85, A86, A106, A109, AFF_1: 8, AFF_1: 25;

            then

             A111: LIN (b,q,c9) by A81, A83, A89, A97, AFF_1: 6, AFF_1: 45;

             LIN (b,q,c) & LIN (b,q,b) by A96, AFF_1: 6, AFF_1: 7;

            then b = q or c = c9 or b in C by A80, A87, A88, A111, AFF_1: 8, AFF_1: 25;

            then LIN (p,q,a) by A82, A85, A94, A101, A99, A110, AFF_1: 2, AFF_1: 6, AFF_1: 45;

            then (p,q) // (p,a) by AFF_1:def 1;

            then (a,c) // (p,a) by A93, A98, AFF_1: 5;

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

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

            then

             A112: LIN (p,a,c) by AFF_1: 6;

             LIN (p,a,b) & LIN (p,a,a) by A94, AFF_1: 6, AFF_1: 7;

            hence contradiction by A91, A106, A112, AFF_1: 8;

          end;

          

           A113: not LIN (p,a,a9)

          proof

            assume

             A114: LIN (p,a,a9);

             LIN (p,a,b) & LIN (p,a,a) by A94, AFF_1: 6, AFF_1: 7;

            then b in A by A78, A83, A84, A106, A108, A114, AFF_1: 8, AFF_1: 25;

            hence contradiction by A81, A85, A89, AFF_1: 45;

          end;

          set A9 = ( Line (a,c)), P9 = ( Line (p,q)), C9 = ( Line (a9,c9));

          

           A115: a <> c by A91, AFF_1: 7;

          then

           A116: A9 is being_line by AFF_1: 24;

          

           A117: (c,c9) // (a,a9) & LIN (q,c,b) by A83, A84, A87, A88, A90, A96, AFF_1: 6, AFF_1: 39;

          

           A118: LIN (p,a9,b9) by A95, AFF_1: 6;

          

           A119: a in A9 & c in A9 by A115, AFF_1: 24;

          

           A120: b <> b9

          proof

            assume b = b9;

            then

             A121: LIN (b,p,a9) by A95, AFF_1: 6;

             LIN (b,p,a) & LIN (b,p,b) by A94, AFF_1: 6, AFF_1: 7;

            then

             A122: b = p or b in A by A78, A83, A84, A108, A121, AFF_1: 8, AFF_1: 25;

            then LIN (p,q,c) by A81, A85, A89, A96, AFF_1: 6, AFF_1: 45;

            then (p,q) // (p,c) by AFF_1:def 1;

            then (a,c) // (p,c) by A93, A98, AFF_1: 5;

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

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

            hence contradiction by A81, A85, A89, A91, A122, AFF_1: 6, AFF_1: 45;

          end;

          

           A123: not LIN (q,c,c9)

          proof

            assume

             A124: LIN (q,c,c9);

             LIN (q,c,b) & LIN (q,c,c) by A96, AFF_1: 6, AFF_1: 7;

            then c = c9 or b in C by A80, A87, A88, A102, A124, AFF_1: 8, AFF_1: 25;

            then

             A125: LIN (q,c,b9) by A82, A85, A97, A99, AFF_1: 6, AFF_1: 45;

             LIN (q,c,b) & LIN (q,c,c) by A96, AFF_1: 6, AFF_1: 7;

            then c in P by A79, A85, A86, A102, A120, A125, AFF_1: 8, AFF_1: 25;

            hence contradiction by A82, A87, A99, AFF_1: 45;

          end;

          

           A126: LIN (q,c9,b9) & LIN (p,a,b) by A94, A97, AFF_1: 6;

          

           A127: a9 <> c9 by A92, AFF_1: 7;

          then

           A128: C9 is being_line by AFF_1: 24;

          

           A129: p in P9 by A93, AFF_1: 24;

          

           A130: A9 <> P9

          proof

            assume A9 = P9;

            then

             A131: LIN (p,a,c) & LIN (p,a,a) by A116, A119, A129, AFF_1: 21;

             LIN (p,a,b) by A94, AFF_1: 6;

            hence contradiction by A91, A106, A131, AFF_1: 8;

          end;

          

           A132: P9 is being_line & q in P9 by A93, AFF_1: 24;

          then

           A133: A9 // P9 by A93, A98, A115, A116, A119, A129, AFF_1: 38;

          

           A134: a9 in C9 & c9 in C9 by A127, AFF_1: 24;

          then A9 <> C9 by A101, A116, A119, AFF_1: 51;

          then A9 // C9 by A77, A127, A116, A128, A119, A129, A132, A134, A100, A133, A130, A120, A123, A113, A117, A126, A118;

          hence contradiction by A101, A119, A134, AFF_1: 39;

        end;

      end;

      hence thesis by A1;

    end;

    theorem :: AFF_3:9

    AP is satisfying_DES2 iff AP is satisfying_DES2_2

    proof

      

       A1: AP is satisfying_DES2 implies AP is satisfying_DES2_2

      proof

        assume

         A2: AP is satisfying_DES2;

        thus AP is satisfying_DES2_2

        proof

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

          assume that

           A3: A is being_line and

           A4: P is being_line and

           A5: C is being_line and

           A6: A <> P and

           A7: A <> C and

           A8: P <> C and

           A9: a in A & a9 in A and

           A10: b in P & b9 in P and

           A11: c in C and

           A12: c9 in C and

           A13: A // C and

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

           A15: not LIN (b9,a9,c9) and

           A16: p <> q and

           A17: a <> a9 and

           A18: LIN (b,a,p) and

           A19: LIN (b9,a9,p) and

           A20: LIN (b,c,q) and

           A21: LIN (b9,c9,q) and

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

           A23: (a,c) // (p,q);

          

           A24: LIN (q,c9,b9) by A21, AFF_1: 6;

          

           A25: c <> c9

          proof

            assume c = c9;

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

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

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

            then c in A by A3, A9, A17, AFF_1: 25;

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

          end;

          

           A26: b <> b9

          proof

             A27:

            now

              assume that

               A28: b = p and b in C;

               LIN (p,q,c) by A20, A28, AFF_1: 6;

              then (p,q) // (p,c) by AFF_1:def 1;

              then (a,c) // (p,c) by A16, A23, AFF_1: 5;

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

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

              hence contradiction by A14, A28, AFF_1: 6;

            end;

            

             A29: LIN (b,p,a) & LIN (b,p,b) by A18, AFF_1: 6, AFF_1: 7;

            assume

             A30: b = b9;

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

            then

             A31: b = p or b in A by A3, A9, A17, A29, AFF_1: 8, AFF_1: 25;

            

             A32: LIN (b,q,c) & LIN (b,q,b) by A20, AFF_1: 6, AFF_1: 7;

             LIN (b,q,c9) by A21, A30, AFF_1: 6;

            then

             A33: b = q or b in C by A5, A11, A12, A25, A32, AFF_1: 8, AFF_1: 25;

            then LIN (q,p,a) by A7, A13, A18, A31, A27, AFF_1: 6, AFF_1: 45;

            then (q,p) // (q,a) by AFF_1:def 1;

            then (p,q) // (q,a) by AFF_1: 4;

            then (a,c) // (q,a) by A16, A23, AFF_1: 5;

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

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

            hence contradiction by A7, A13, A14, A31, A33, A27, AFF_1: 6, AFF_1: 45;

          end;

          

           A34: a <> p

          proof

            assume

             A35: a = p;

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

            then

             A36: LIN (c,q,a) by AFF_1: 6;

             LIN (c,q,b) & LIN (c,q,c) by A20, AFF_1: 6, AFF_1: 7;

            then q = c by A14, A36, AFF_1: 8;

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

            then

             A37: c = c9 or b9 in C by A5, A11, A12, AFF_1: 25;

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

            then b9 in A by A3, A9, A17, AFF_1: 25;

            then (c,a) // (c,a9) by A7, A13, A22, A37, AFF_1: 4, AFF_1: 45;

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

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

            then c in A by A3, A9, A17, AFF_1: 25;

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

          end;

          

           A38: q <> c

          proof

            assume q = c;

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

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

            then

             A39: LIN (p,a,c) by AFF_1: 6;

             LIN (p,a,b) & LIN (p,a,a) by A18, AFF_1: 6, AFF_1: 7;

            hence contradiction by A14, A34, A39, AFF_1: 8;

          end;

          

           A40: LIN (q,c,b) by A20, AFF_1: 6;

          set A9 = ( Line (a,c)), P9 = ( Line (p,q)), C9 = ( Line (a9,c9));

          

           A41: a <> c by A14, AFF_1: 7;

          then

           A42: c in A9 by AFF_1: 24;

          

           A43: a9 <> p

          proof

            assume

             A44: a9 = p;

            (a9,c9) // (p,q) by A22, A23, A41, AFF_1: 5;

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

            then

             A45: LIN (c9,q,a9) by AFF_1: 6;

             LIN (c9,q,b9) & LIN (c9,q,c9) by A21, AFF_1: 6, AFF_1: 7;

            then q = c9 by A15, A45, AFF_1: 8;

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

            then

             A46: b in C by A5, A11, A12, A25, AFF_1: 25;

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

            then b in A by A3, A9, A17, AFF_1: 25;

            hence contradiction by A7, A13, A46, AFF_1: 45;

          end;

          

           A47: c9 <> q

          proof

            assume c9 = q;

            then (a9,c9) // (p,c9) by A22, A23, A41, AFF_1: 5;

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

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

            then

             A48: LIN (p,a9,c9) by AFF_1: 6;

             LIN (p,a9,b9) & LIN (p,a9,a9) by A19, AFF_1: 6, AFF_1: 7;

            hence contradiction by A15, A43, A48, AFF_1: 8;

          end;

          

           A49: not LIN (q,c9,c)

          proof

            

             A50: LIN (q,c,c) by AFF_1: 7;

            assume

             A51: LIN (q,c9,c);

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

            then

             A52: b9 in C by A5, A11, A12, A25, A47, A24, A51, AFF_1: 8, AFF_1: 25;

             LIN (q,c,c9) by A51, AFF_1: 6;

            then b in C by A5, A11, A12, A38, A25, A40, A50, AFF_1: 8, AFF_1: 25;

            hence contradiction by A4, A5, A8, A10, A26, A52, AFF_1: 18;

          end;

          

           A53: LIN (p,a,b) by A18, AFF_1: 6;

          

           A54: LIN (p,a9,b9) by A19, AFF_1: 6;

          

           A55: not LIN (p,a9,a)

          proof

            

             A56: LIN (p,a,a) by AFF_1: 7;

            assume

             A57: LIN (p,a9,a);

             LIN (p,a9,a9) by AFF_1: 7;

            then

             A58: b9 in A by A3, A9, A17, A43, A54, A57, AFF_1: 8, AFF_1: 25;

             LIN (p,a,a9) by A57, AFF_1: 6;

            then b in A by A3, A9, A17, A34, A53, A56, AFF_1: 8, AFF_1: 25;

            hence contradiction by A3, A4, A6, A10, A26, A58, AFF_1: 18;

          end;

          

           A59: (a9,a) // (c9,c) by A9, A11, A12, A13, AFF_1: 39;

          

           A60: q in P9 by A16, AFF_1: 24;

          

           A61: a9 <> c9 by A15, AFF_1: 7;

          then

           A62: a9 in C9 by AFF_1: 24;

          

           A63: A9 is being_line & a in A9 by A41, AFF_1: 24;

          

           A64: C9 <> A9

          proof

            assume C9 = A9;

            then LIN (a,a9,c) by A63, A42, A62, AFF_1: 21;

            then c in A by A3, A9, A17, AFF_1: 25;

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

          end;

          

           A65: p in P9 by A16, AFF_1: 24;

          

           A66: P9 <> A9

          proof

            assume P9 = A9;

            then

             A67: LIN (p,a,c) & LIN (p,a,a) by A63, A42, A65, AFF_1: 21;

             LIN (p,a,b) by A18, AFF_1: 6;

            hence contradiction by A14, A34, A67, AFF_1: 8;

          end;

          

           A68: c9 in C9 by A61, AFF_1: 24;

          

           A69: P9 is being_line by A16, AFF_1: 24;

          

           A70: C9 <> P9

          proof

            assume C9 = P9;

            then

             A71: LIN (p,a9,c9) & LIN (p,a9,a9) by A69, A65, A62, A68, AFF_1: 21;

             LIN (p,a9,b9) by A19, AFF_1: 6;

            hence contradiction by A15, A43, A71, AFF_1: 8;

          end;

          

           A72: C9 is being_line by A61, AFF_1: 24;

          (a9,c9) // (p,q) by A22, A23, A41, AFF_1: 5;

          then

           A73: C9 // P9 by A16, A61, A69, A72, A65, A60, A62, A68, AFF_1: 38;

          C9 // A9 by A22, A41, A61, A72, A63, A42, A62, A68, AFF_1: 38;

          then (a9,a) // (b9,b) by A2, A61, A26, A69, A72, A63, A42, A65, A60, A62, A68, A73, A64, A70, A66, A54, A53, A24, A40, A55, A49, A59;

          hence thesis by A3, A4, A9, A10, A17, A26, AFF_1: 38;

        end;

      end;

      AP is satisfying_DES2_2 implies AP is satisfying_DES2

      proof

        assume

         A74: AP is satisfying_DES2_2;

        thus AP is satisfying_DES2

        proof

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

          assume that

           A75: A is being_line and P is being_line and

           A76: C is being_line and

           A77: A <> P and

           A78: A <> C and

           A79: P <> C and

           A80: a in A & a9 in A and

           A81: b in P and

           A82: b9 in P and

           A83: c in C and

           A84: c9 in C and

           A85: A // P and

           A86: A // C and

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

           A88: not LIN (b9,a9,c9) and

           A89: p <> q and

           A90: a <> a9 and

           A91: LIN (b,a,p) and

           A92: LIN (b9,a9,p) and

           A93: LIN (b,c,q) and

           A94: LIN (b9,c9,q) and

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

          

           A96: LIN (p,a,b) by A91, AFF_1: 6;

          set A9 = ( Line (a,c)), P9 = ( Line (p,q)), C9 = ( Line (a9,c9));

          

           A97: q in P9 by A89, AFF_1: 24;

          

           A98: a <> p

          proof

            assume a = p;

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

            then b9 in A by A75, A80, A90, AFF_1: 25;

            hence contradiction by A77, A82, A85, AFF_1: 45;

          end;

          

           A99: not LIN (p,a,a9)

          proof

            

             A100: LIN (p,a,a) by AFF_1: 7;

            assume LIN (p,a,a9);

            then b in A by A75, A80, A90, A98, A96, A100, AFF_1: 8, AFF_1: 25;

            hence contradiction by A77, A81, A85, AFF_1: 45;

          end;

          

           A101: LIN (q,c9,b9) & LIN (p,a9,b9) by A92, A94, AFF_1: 6;

          

           A102: a <> c by A87, AFF_1: 7;

          then

           A103: A9 is being_line by AFF_1: 24;

          

           A104: C // P by A85, A86, AFF_1: 44;

          then

           A105: (c,c9) // (b,b9) by A81, A82, A83, A84, AFF_1: 39;

          

           A106: c <> c9

          proof

            assume c = c9;

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

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

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

            then c in A by A75, A80, A90, AFF_1: 25;

            hence contradiction by A78, A83, A86, AFF_1: 45;

          end;

          

           A107: b <> b9

          proof

            

             A108: LIN (b,p,a) & LIN (b,p,b) by A91, AFF_1: 6, AFF_1: 7;

            assume

             A109: b = b9;

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

            then

             A110: b = p or b in A by A75, A80, A90, A108, AFF_1: 8, AFF_1: 25;

            

             A111: LIN (b,q,c) & LIN (b,q,b) by A93, AFF_1: 6, AFF_1: 7;

             LIN (b,q,c9) by A94, A109, AFF_1: 6;

            then b = q or b in C by A76, A83, A84, A106, A111, AFF_1: 8, AFF_1: 25;

            hence contradiction by A77, A79, A81, A85, A89, A104, A110, AFF_1: 45;

          end;

          

           A112: a in A9 & c in A9 by A102, AFF_1: 24;

          

           A113: P9 is being_line & (c,c9) // (a,a9) by A80, A83, A84, A86, A89, AFF_1: 24, AFF_1: 39;

          

           A114: p in P9 by A89, AFF_1: 24;

          

           A115: a9 <> c9 by A88, AFF_1: 7;

          then

           A116: a9 in C9 by AFF_1: 24;

          

           A117: A9 <> C9

          proof

            assume A9 = C9;

            then LIN (a,a9,c) by A103, A112, A116, AFF_1: 21;

            then c in A by A75, A80, A90, AFF_1: 25;

            hence contradiction by A78, A83, A86, AFF_1: 45;

          end;

          

           A118: q <> c

          proof

            assume q = c;

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

            then b9 in C by A76, A83, A84, A106, AFF_1: 25;

            hence contradiction by A79, A82, A104, AFF_1: 45;

          end;

          

           A119: A9 <> P9

          proof

            assume A9 = P9;

            then

             A120: LIN (c,q,a) & LIN (c,q,c) by A103, A112, A97, AFF_1: 21;

             LIN (c,q,b) by A93, AFF_1: 6;

            hence contradiction by A87, A118, A120, AFF_1: 8;

          end;

          

           A121: LIN (q,c,b) by A93, AFF_1: 6;

          

           A122: not LIN (q,c,c9)

          proof

            

             A123: LIN (q,c,c) by AFF_1: 7;

            assume LIN (q,c,c9);

            then b in C by A76, A83, A84, A106, A118, A121, A123, AFF_1: 8, AFF_1: 25;

            hence contradiction by A79, A81, A104, AFF_1: 45;

          end;

          

           A124: C9 is being_line & c9 in C9 by A115, AFF_1: 24;

          then A9 // C9 by A95, A102, A115, A103, A112, A116, AFF_1: 38;

          then A9 // P9 by A74, A102, A107, A103, A112, A114, A97, A116, A124, A113, A105, A121, A96, A101, A119, A117, A122, A99;

          hence thesis by A112, A114, A97, AFF_1: 39;

        end;

      end;

      hence thesis by A1;

    end;

    theorem :: AFF_3:10

    AP is satisfying_DES1_3 implies AP is satisfying_DES2_1

    proof

      assume

       A1: AP is satisfying_DES1_3;

      let A, P, C, a, a9, b, b9, c, c9, p, q such that

       A2: A is being_line and

       A3: P is being_line and

       A4: C is being_line and

       A5: A <> P and

       A6: A <> C and

       A7: P <> 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 // P and

       A15: A // C and

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

       A17: not LIN (b9,a9,c9) and

       A18: p <> q and

       A19: LIN (b,a,p) and

       A20: LIN (b9,a9,p) and

       A21: LIN (b,c,q) and

       A22: LIN (b9,c9,q) and

       A23: (a,c) // (p,q);

      

       A24: P // C by A14, A15, AFF_1: 44;

      set K = ( Line (p,q)), M = ( Line (a,c)), N = ( Line (a9,c9));

      

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

      then

       A26: a in M by AFF_1: 24;

      

       A27: (c,c9) // (a,a9) & LIN (q,c,b) by A8, A9, A12, A13, A15, A21, AFF_1: 6, AFF_1: 39;

      

       A28: LIN (p,a9,b9) by A20, AFF_1: 6;

      C // P by A14, A15, AFF_1: 44;

      then

       A29: (c,c9) // (b,b9) by A10, A11, A12, A13, AFF_1: 39;

      

       A30: LIN (q,c9,b9) & LIN (p,a,b) by A19, A22, AFF_1: 6;

      

       A31: c in M by A25, AFF_1: 24;

      assume

       A32: not thesis;

      

       A33: c <> q

      proof

        assume

         A34: c = q;

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

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

        then

         A35: LIN (p,a,c) by AFF_1: 6;

         LIN (p,a,b) & LIN (p,a,a) by A19, AFF_1: 6, AFF_1: 7;

        then p = a by A16, A35, AFF_1: 8;

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

        then

         A36: a = a9 or b9 in A by A2, A8, A9, AFF_1: 25;

         LIN (c,c9,b9) by A22, A34, AFF_1: 6;

        then c = c9 or b9 in C by A4, A12, A13, AFF_1: 25;

        hence contradiction by A5, A7, A11, A14, A32, A24, A36, AFF_1: 2, AFF_1: 45;

      end;

      

       A37: c <> c9

      proof

         A38:

        now

          assume

           A39: p = b;

           LIN (b,q,c) by A21, AFF_1: 6;

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

          then (a,c) // (b,c) or b = q by A23, A39, AFF_1: 5;

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

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

          hence contradiction by A16, AFF_1: 6;

        end;

        

         A40: LIN (q,c,b) & LIN (q,c,c) by A21, AFF_1: 6, AFF_1: 7;

        assume

         A41: c = c9;

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

        then b = b9 or c in P by A3, A10, A11, A33, A40, AFF_1: 8, AFF_1: 25;

        then

         A42: LIN (p,b,a9) by A7, A12, A20, A24, AFF_1: 6, AFF_1: 45;

         LIN (p,b,a) & LIN (p,b,b) by A19, AFF_1: 6, AFF_1: 7;

        then a = a9 or b in A by A2, A8, A9, A42, A38, AFF_1: 8, AFF_1: 25;

        hence contradiction by A5, A10, A14, A32, A41, AFF_1: 2, AFF_1: 45;

      end;

      

       A43: b <> b9

      proof

        assume b = b9;

        then

         A44: LIN (q,b,c9) by A22, AFF_1: 6;

         LIN (q,b,c) & LIN (q,b,b) by A21, AFF_1: 6, AFF_1: 7;

        then

         A45: q = b or b in C by A4, A12, A13, A37, A44, AFF_1: 8, AFF_1: 25;

        (b,a) // (b,p) by A19, AFF_1:def 1;

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

        then (a,c) // (a,b) or p = b by A7, A10, A23, A24, A45, AFF_1: 5, AFF_1: 45;

        then LIN (a,c,b) by A7, A10, A18, A24, A45, AFF_1: 45, AFF_1:def 1;

        hence contradiction by A16, AFF_1: 6;

      end;

      

       A46: not LIN (q,c,c9)

      proof

        assume

         A47: LIN (q,c,c9);

         LIN (q,c,b) & LIN (q,c,c) by A21, AFF_1: 6, AFF_1: 7;

        then b in C by A4, A12, A13, A33, A37, A47, AFF_1: 8, AFF_1: 25;

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

      end;

      

       A48: a9 <> c9 by A17, AFF_1: 7;

      then

       A49: N is being_line by AFF_1: 24;

      

       A50: p <> a

      proof

        assume p = a;

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

        then

         A51: LIN (c,q,a) by AFF_1: 6;

         LIN (c,q,b) & LIN (c,q,c) by A21, AFF_1: 6, AFF_1: 7;

        hence contradiction by A16, A33, A51, AFF_1: 8;

      end;

      

       A52: not LIN (p,a,a9)

      proof

        assume

         A53: LIN (p,a,a9);

         LIN (p,a,b) & LIN (p,a,a) by A19, AFF_1: 6, AFF_1: 7;

        then a = a9 or b in A by A2, A8, A9, A50, A53, AFF_1: 8, AFF_1: 25;

        then

         A54: LIN (p,a,b9) by A5, A10, A14, A20, AFF_1: 6, AFF_1: 45;

         LIN (p,a,b) & LIN (p,a,a) by A19, AFF_1: 6, AFF_1: 7;

        then a in P by A3, A10, A11, A43, A50, A54, AFF_1: 8, AFF_1: 25;

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

      end;

      

       A55: M is being_line by A25, AFF_1: 24;

      

       A56: K is being_line & q in K by A18, AFF_1: 24;

       A57:

      now

        assume M = K;

        then

         A58: LIN (q,c,a) & LIN (q,c,c) by A56, A26, A31, AFF_1: 21;

         LIN (q,c,b) by A21, AFF_1: 6;

        hence contradiction by A16, A33, A58, AFF_1: 8;

      end;

      

       A59: c9 in N by A48, AFF_1: 24;

      

       A60: a9 in N by A48, AFF_1: 24;

      then

      consider x such that

       A61: x in M and

       A62: x in N by A32, A55, A49, A26, A31, A59, AFF_1: 39, AFF_1: 58;

       A63:

      now

        assume x = c;

        then N = C by A4, A12, A13, A37, A49, A59, A62, AFF_1: 18;

        hence contradiction by A6, A9, A15, A60, AFF_1: 45;

      end;

      

       A64: p in K by A18, AFF_1: 24;

      then

       A65: M // K by A18, A23, A25, A55, A56, A26, A31, AFF_1: 38;

       A66:

      now

        assume x = c9;

        then M = C by A4, A12, A13, A37, A55, A31, A61, AFF_1: 18;

        hence contradiction by A6, A8, A15, A26, AFF_1: 45;

      end;

      M <> N by A32, A55, A26, A31, A60, A59, AFF_1: 51;

      then x in K by A1, A18, A25, A55, A49, A64, A56, A26, A31, A60, A59, A61, A62, A29, A27, A30, A28, A43, A63, A66, A46, A52;

      hence contradiction by A65, A61, A57, AFF_1: 45;

    end;