conmetr.miz



    begin

    reserve X for OrtAfPl;

    reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1,c2,c3,d,d1,d2,d3,d4,e1,e2 for Element of X;

    reserve a29,a39,b29,x9 for Element of the AffinStruct of X;

    reserve A,K,M,N for Subset of X;

    reserve A9,K9 for Subset of the AffinStruct of X;

    definition

      let X;

      :: CONMETR:def1

      attr X is satisfying_OPAP means for o, a1, a2, a3, b1, b2, b3, M, N st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & (a3,b2) // (a2,b1) & (a3,b3) // (a1,b1) holds (a1,b2) // (a2,b3);

      :: CONMETR:def2

      attr X is satisfying_PAP means for o, a1, a2, a3, b1, b2, b3, M, N st M is being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & (a3,b2) // (a2,b1) & (a3,b3) // (a1,b1) holds (a1,b2) // (a2,b3);

      :: CONMETR:def3

      attr X is satisfying_MH1 means for a1, a2, a3, a4, b1, b2, b3, b4, M, N st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a2 in M & not a4 in M & (a1,a2) _|_ (b1,b2) & (a2,a3) _|_ (b2,b3) & (a3,a4) _|_ (b3,b4) holds (a1,a4) _|_ (b1,b4);

      :: CONMETR:def4

      attr X is satisfying_MH2 means for a1, a2, a3, a4, b1, b2, b3, b4, M, N st M _|_ N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a2 in M & not a4 in M & (a1,a2) _|_ (b1,b2) & (a2,a3) _|_ (b2,b3) & (a3,a4) _|_ (b3,b4) holds (a1,a4) _|_ (b1,b4);

      :: CONMETR:def5

      attr X is satisfying_TDES means for o, a, a1, b, b1, c, c1 st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN (b,b1,a) & not LIN (b,b1,c) & LIN (o,a,a1) & LIN (o,b,b1) & LIN (o,c,c1) & (a,b) // (a1,b1) & (a,b) // (o,c) & (b,c) // (b1,c1) holds (a,c) // (a1,c1);

      :: CONMETR:def6

      attr X is satisfying_SCH means for a1, a2, a3, a4, b1, b2, b3, b4, M, N st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & (a3,a2) // (b3,b2) & (a2,a1) // (b2,b1) & (a1,a4) // (b1,b4) holds (a3,a4) // (b3,b4);

      :: CONMETR:def7

      attr X is satisfying_OSCH means for a1, a2, a3, a4, b1, b2, b3, b4, M, N st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & (a3,a2) // (b3,b2) & (a2,a1) // (b2,b1) & (a1,a4) // (b1,b4) holds (a3,a4) // (b3,b4);

      :: CONMETR:def8

      attr X is satisfying_des means for a, a1, b, b1, c, c1 st not LIN (a,a1,b) & not LIN (a,a1,c) & (a,a1) // (b,b1) & (a,a1) // (c,c1) & (a,b) // (a1,b1) & (a,c) // (a1,c1) holds (b,c) // (b1,c1);

    end

    theorem :: CONMETR:1

    

     Th1: ex a, b, c st LIN (a,b,c) & a <> b & b <> c & c <> a

    proof

      consider a,p be Element of X such that

       A1: a <> p by ANALMETR: 39;

      consider b such that

       A2: (a,p) _|_ (p,b) and

       A3: p <> b by ANALMETR: 39;

      reconsider a9 = a, b9 = b, p9 = p as Element of the AffinStruct of X;

      consider c such that

       A4: (p,c) _|_ (a,b) and

       A5: LIN (a,b,c) by ANALMETR: 69;

      take a, b, c;

      thus LIN (a,b,c) by A5;

      thus a <> b

      proof

        assume not thesis;

        then (a,p) _|_ (a,p) by A2, ANALMETR: 61;

        hence contradiction by A1, ANALMETR: 39;

      end;

      thus b <> c

      proof

        assume not thesis;

        then (a,p) // (a,b) by A2, A3, A4, ANALMETR: 63;

        then LIN (a,p,b) by ANALMETR:def 10;

        then LIN (a9,p9,b9) by ANALMETR: 40;

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

        then LIN (p,a,b) by ANALMETR: 40;

        then (p,a) // (p,b) by ANALMETR:def 10;

        then (a,p) _|_ (p,a) by A2, A3, ANALMETR: 62;

        then (a,p) _|_ (a,p) by ANALMETR: 61;

        hence contradiction by A1, ANALMETR: 39;

      end;

      assume not thesis;

      then (a,p) _|_ (a,b) by A4, ANALMETR: 61;

      then (p,b) // (a,b) by A1, A2, ANALMETR: 63;

      then (b,p) // (b,a) by ANALMETR: 59;

      then LIN (b,p,a) by ANALMETR:def 10;

      then LIN (b9,p9,a9) by ANALMETR: 40;

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

      then LIN (p,a,b) by ANALMETR: 40;

      then (p,a) // (p,b) by ANALMETR:def 10;

      then (a,p) _|_ (p,a) by A2, A3, ANALMETR: 62;

      then (a,p) _|_ (a,p) by ANALMETR: 61;

      hence contradiction by A1, ANALMETR: 39;

    end;

    theorem :: CONMETR:2

    

     Th2: for a, b holds ex c st LIN (a,b,c) & a <> c & b <> c

    proof

      let a, b;

      consider p,q,r be Element of X such that

       A1: LIN (p,q,r) and

       A2: p <> q and

       A3: q <> r and

       A4: r <> p by Th1;

      reconsider a9 = a, b9 = b, p9 = p, q9 = q, r9 = r as Element of the AffinStruct of X;

       LIN (p9,q9,r9) by A1, ANALMETR: 40;

      then

      consider c9 be Element of the AffinStruct of X such that

       A5: LIN (a9,b9,c9) and

       A6: a9 <> c9 and

       A7: b9 <> c9 by A2, A3, A4, TRANSLAC: 1;

      reconsider c = c9 as Element of X;

       LIN (a,b,c) by A5, ANALMETR: 40;

      hence thesis by A6, A7;

    end;

    theorem :: CONMETR:3

    

     Th3: for A, a st A is being_line holds ex K st a in K & A _|_ K

    proof

      let A, a;

      assume A is being_line;

      then

      consider b, c such that

       A1: b <> c and

       A2: A = ( Line (b,c)) by ANALMETR:def 12;

      consider d such that

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

       A4: a <> d by ANALMETR: 39;

      reconsider a9 = a, d9 = d as Element of the AffinStruct of X;

      take K = ( Line (a,d));

      K = ( Line (a9,d9)) by ANALMETR: 41;

      hence a in K by AFF_1: 15;

      thus thesis by A1, A2, A3, A4, ANALMETR: 45;

    end;

    theorem :: CONMETR:4

    

     Th4: A is being_line & a in A & b in A & c in A implies LIN (a,b,c)

    proof

      assume that

       A1: A is being_line and

       A2: a in A and

       A3: b in A and

       A4: c in A;

      reconsider a9 = a, b9 = b, c9 = c as Element of the AffinStruct of X;

      reconsider A9 = A as Subset of the AffinStruct of X;

      A9 is being_line by A1, ANALMETR: 43;

      then LIN (a9,b9,c9) by A2, A3, A4, AFF_1: 21;

      hence thesis by ANALMETR: 40;

    end;

    theorem :: CONMETR:5

    

     Th5: A is being_line & M is being_line & a in A & b in A & a in M & b in M implies a = b or A = M

    proof

      assume that

       A1: A is being_line and

       A2: M is being_line and

       A3: a in A and

       A4: b in A and

       A5: a in M and

       A6: b in M;

      reconsider A9 = A, M9 = M as Subset of the AffinStruct of X;

      

       A7: M9 is being_line by A2, ANALMETR: 43;

      assume

       A8: a <> b;

      A9 is being_line by A1, ANALMETR: 43;

      hence thesis by A3, A4, A5, A6, A8, A7, AFF_1: 18;

    end;

    theorem :: CONMETR:6

    

     Th6: for a, b, c, d, M holds for M9 be Subset of the AffinStruct of X, c9,d9 be Element of the AffinStruct of X st c = c9 & d = d9 & M = M9 & a in M & b in M & (c9,d9) // M9 holds (c,d) // (a,b)

    proof

      let a, b, c, d, M;

      let M9 be Subset of the AffinStruct of X, c9,d9 be Element of the AffinStruct of X such that

       A1: c = c9 and

       A2: d = d9 and

       A3: M = M9 and

       A4: a in M and

       A5: b in M and

       A6: (c9,d9) // M9;

      reconsider a9 = a, b9 = b as Element of the AffinStruct of X;

      

       A7: M9 is being_line by A6, AFF_1: 26;

      then (a9,b9) // M9 by A3, A4, A5, AFF_1: 52;

      then (c9,d9) // (a9,b9) by A7, A6, AFF_1: 31;

      hence thesis by A1, A2, ANALMETR: 36;

    end;

    theorem :: CONMETR:7

    

     Th7: X is satisfying_TDES implies the AffinStruct of X is Moufangian

    proof

      assume

       A1: X is satisfying_TDES;

      let K9 be Subset of the AffinStruct of X;

      let o9,a9,b9,c9,a19,b19,c19 be Element of the AffinStruct of X;

      assume that

       A2: K9 is being_line and

       A3: o9 in K9 and

       A4: c9 in K9 and

       A5: c19 in K9 and

       A6: not a9 in K9 and

       A7: o9 <> c9 and

       A8: a9 <> b9 and

       A9: LIN (o9,a9,a19) and

       A10: LIN (o9,b9,b19) and

       A11: (a9,b9) // (a19,b19) and

       A12: (a9,c9) // (a19,c19) and

       A13: (a9,b9) // K9;

      reconsider K = K9 as Subset of X;

      reconsider o = o9, a = a9, a1 = a19, b = b9, b1 = b19, c = c9, c1 = c19 as Element of X;

      

       A14: (a,c) // (a1,c1) by A12, ANALMETR: 36;

      

       A15: (a,b) // (a1,b1) by A11, ANALMETR: 36;

      now

         A16:

        now

          assume

           A17: o <> a1;

          

           A18: o <> a & o <> b & o <> c & o <> c1 & o <> b1

          proof

             A19:

            now

              (o9,c9) // K9 by A2, A3, A4, AFF_1: 23;

              then

               A20: (a9,b9) // (o9,c9) by A2, A13, AFF_1: 31;

              assume o = b1;

              then (a19,o9) // (o9,c9) by A8, A11, A20, DIRAF: 40;

              then (o9,c9) // (o9,a19) by AFF_1: 4;

              then LIN (o9,c9,a19) by AFF_1:def 1;

              then

               A21: a19 in K9 by A2, A3, A4, A7, AFF_1: 25;

               LIN (o9,a19,a9) by A9, AFF_1: 6;

              hence contradiction by A2, A3, A6, A17, A21, AFF_1: 25;

            end;

             A22:

            now

              (o9,a9) // (o9,a19) by A9, AFF_1:def 1;

              then

               A23: (o9,a19) // (a9,o9) by AFF_1: 4;

              assume o = c1;

              then (o9,a19) // (a9,c9) by A12, AFF_1: 4;

              then (a9,c9) // (a9,o9) by A17, A23, DIRAF: 40;

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

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

              hence contradiction by A2, A3, A4, A6, A7, AFF_1: 25;

            end;

            assume o = a or o = b or o = c or o = c1 or o = b1;

            hence contradiction by A3, A6, A7, A13, A22, A19, AFF_1: 35;

          end;

           A24:

          now

            assume

             A25: a <> a19;

            

             A26: not LIN (a,a1,b) & not LIN (a,a1,c)

            proof

               A27:

              now

                 LIN (a9,a19,o9) by A9, AFF_1: 6;

                then (a9,a19) // (a9,o9) by AFF_1:def 1;

                then

                 A28: (a,a1) // (a,o) by ANALMETR: 36;

                assume LIN (a,a1,b);

                then (a,a1) // (a,b) by ANALMETR:def 10;

                then (a,b) // (a,o) by A25, A28, ANALMETR: 60;

                then

                 A29: (a,b) // (o,a) by ANALMETR: 59;

                (a9,b9) // (o9,c9) by A2, A3, A4, A7, A13, AFF_1: 27;

                then (a,b) // (o,c) by ANALMETR: 36;

                then (o,c) // (o,a) by A8, A29, ANALMETR: 60;

                then LIN (o,c,a) by ANALMETR:def 10;

                then LIN (o9,c9,a9) by ANALMETR: 40;

                hence contradiction by A2, A3, A4, A6, A7, AFF_1: 25;

              end;

               A30:

              now

                 LIN (a9,a19,o9) by A9, AFF_1: 6;

                then (a9,a19) // (a9,o9) by AFF_1:def 1;

                then

                 A31: (a,a1) // (a,o) by ANALMETR: 36;

                assume LIN (a,a1,c);

                then (a,a1) // (a,c) by ANALMETR:def 10;

                then (a,c) // (a,o) by A25, A31, ANALMETR: 60;

                then LIN (a,c,o) by ANALMETR:def 10;

                then LIN (a9,c9,o9) by ANALMETR: 40;

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

                hence contradiction by A2, A3, A4, A6, A7, AFF_1: 25;

              end;

              assume LIN (a,a1,b) or LIN (a,a1,c);

              hence contradiction by A27, A30;

            end;

            

             A32: LIN (o,b,b1) by A10, ANALMETR: 40;

            (o9,c9) // (o9,c19) by A2, A3, A4, A5, AFF_1: 39, AFF_1: 41;

            then (o,c) // (o,c1) by ANALMETR: 36;

            then

             A33: LIN (o,c,c1) by ANALMETR:def 10;

            (o9,c9) // K9 by A2, A3, A4, AFF_1: 40, AFF_1: 41;

            then (a9,b9) // (o9,c9) by A2, A13, AFF_1: 31;

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

            then

             A34: (b,a) // (o,c) by ANALMETR: 36;

            

             A35: (b,a) // (b1,a1) by A15, ANALMETR: 59;

             LIN (o,a,a1) by A9, ANALMETR: 40;

            then (b,c) // (b1,c1) by A1, A14, A17, A18, A26, A32, A33, A35, A34;

            hence thesis by ANALMETR: 36;

          end;

          now

            

             A36: not LIN (o9,a9,c9)

            proof

              assume LIN (o9,a9,c9);

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

              hence contradiction by A2, A3, A4, A6, A7, AFF_1: 25;

            end;

            assume

             A37: a = a1;

            (o9,c9) // (o9,c19) by A2, A3, A4, A5, AFF_1: 39, AFF_1: 41;

            then LIN (o9,c9,c19) by AFF_1:def 1;

            then

             A38: c9 = c19 by A12, A37, A36, AFF_1: 14;

             not LIN (o9,a9,b9)

            proof

              assume LIN (o9,a9,b9);

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

              then

               A39: (a9,b9) // (a9,o9) by AFF_1:def 1;

              (o9,c9) // K9 by A2, A3, A4, AFF_1: 23;

              then (a9,b9) // (o9,c9) by A2, A13, AFF_1: 31;

              then (a9,o9) // (o9,c9) by A8, A39, DIRAF: 40;

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

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

              hence contradiction by A2, A3, A4, A6, A7, AFF_1: 25;

            end;

            then b9 = b19 by A10, A11, A37, AFF_1: 14;

            hence thesis by A38, AFF_1: 2;

          end;

          hence thesis by A24;

        end;

        assume

         A40: not b in K;

        

         A41: o = a1 implies o = b1 & o = c1

        proof

          assume that

           A42: o = a1 and

           A43: o <> b1 or o <> c1;

           A44:

          now

            

             A45: (o9,c19) // (a9,c9) by A12, A42, AFF_1: 4;

            assume

             A46: o <> c1;

            (o9,c19) // (o9,c9) by A2, A3, A4, A5, AFF_1: 39, AFF_1: 41;

            then (a9,c9) // (o9,c9) by A46, A45, DIRAF: 40;

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

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

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

            hence contradiction by A2, A3, A4, A6, A7, AFF_1: 25;

          end;

          now

            (o9,c9) // K9 by A2, A3, A4, AFF_1: 23;

            then (a9,b9) // (o9,c9) by A2, A13, AFF_1: 31;

            then (o9,c9) // (o9,b19) by A8, A11, A42, DIRAF: 40;

            then LIN (o9,c9,b19) by AFF_1:def 1;

            then

             A47: b19 in K9 by A2, A3, A4, A7, AFF_1: 25;

            assume

             A48: o <> b1;

             LIN (o9,b19,b9) by A10, AFF_1: 6;

            hence contradiction by A2, A3, A40, A48, A47, AFF_1: 25;

          end;

          hence contradiction by A43, A44;

        end;

        now

          assume o = a1;

          then (b,c) // (b1,c1) by A41, ANALMETR: 39;

          hence thesis by ANALMETR: 36;

        end;

        hence thesis by A16;

      end;

      hence thesis by A6, A13, AFF_1: 35;

    end;

    theorem :: CONMETR:8

    

     Th8: the AffinStruct of X is translational implies X is satisfying_des

    proof

      assume

       A1: the AffinStruct of X is translational;

      let a, a1, b, b1, c, c1;

      assume that

       A2: not LIN (a,a1,b) and

       A3: not LIN (a,a1,c) and

       A4: (a,a1) // (b,b1) and

       A5: (a,a1) // (c,c1) and

       A6: (a,b) // (a1,b1) and

       A7: (a,c) // (a1,c1);

      reconsider a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1 as Element of the AffinStruct of X;

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

      then

      consider A9 be Subset of the AffinStruct of X such that

       A8: A9 is being_line and

       A9: a9 in A9 and

       A10: a19 in A9 and a19 in A9 by AFF_1: 21;

      

       A11: (a9,b9) // (a19,b19) by A6, ANALMETR: 36;

      (b,b1) // (a,a1) by A4, ANALMETR: 59;

      then

       A12: (b9,b19) // (a9,a19) by ANALMETR: 36;

      

       A13: a9 <> a19

      proof

        assume a9 = a19;

        then LIN (a9,a19,b9) by AFF_1: 7;

        hence contradiction by A2, ANALMETR: 40;

      end;

      then for x9 holds x9 in A9 iff LIN (a9,a19,x9) by A8, A9, A10, AFF_1: 21, AFF_1: 25;

      then A9 = ( Line (a9,a19)) by AFF_1:def 2;

      then

       A14: (b9,b19) // A9 by A13, A12, AFF_1:def 4;

      

       A15: (a9,c9) // (a19,c19) by A7, ANALMETR: 36;

      (c,c1) // (a,a1) by A5, ANALMETR: 59;

      then

       A16: (c9,c19) // (a9,a19) by ANALMETR: 36;

      

       A17: a9 <> a19

      proof

        assume a9 = a19;

        then LIN (a9,a19,b9) by AFF_1: 7;

        hence contradiction by A2, ANALMETR: 40;

      end;

      then for x9 holds x9 in A9 iff LIN (a9,a19,x9) by A8, A9, A10, AFF_1: 21, AFF_1: 25;

      then A9 = ( Line (a9,a19)) by AFF_1:def 2;

      then

       A18: (c9,c19) // A9 by A17, A16, AFF_1:def 4;

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

      then

      consider N9 be Subset of the AffinStruct of X such that

       A19: N9 is being_line and

       A20: c9 in N9 and

       A21: c19 in N9 and c19 in N9 by AFF_1: 21;

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

      then

      consider M9 be Subset of the AffinStruct of X such that

       A22: M9 is being_line and

       A23: b9 in M9 and

       A24: b19 in M9 and b19 in M9 by AFF_1: 21;

      

       A25: A9 <> M9 & A9 <> N9

      proof

        assume A9 = M9 or A9 = N9;

        then LIN (a9,a19,b9) or LIN (a9,a19,c9) by A8, A9, A10, A23, A20, AFF_1: 21;

        hence contradiction by A2, A3, ANALMETR: 40;

      end;

      

       A26: c9 <> c19

      proof

        assume c9 = c19;

        then (c,a) // (c,a1) by A7, ANALMETR: 59;

        then LIN (c,a,a1) by ANALMETR:def 10;

        then LIN (c9,a9,a19) by ANALMETR: 40;

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

        hence contradiction by A3, ANALMETR: 40;

      end;

      then for x9 holds x9 in N9 iff LIN (c9,c19,x9) by A19, A20, A21, AFF_1: 21, AFF_1: 25;

      then N9 = ( Line (c9,c19)) by AFF_1:def 2;

      then

       A27: A9 // N9 by A18, A26, AFF_1:def 5;

      

       A28: b9 <> b19

      proof

        assume b9 = b19;

        then (b,a) // (b,a1) by A6, ANALMETR: 59;

        then LIN (b,a,a1) by ANALMETR:def 10;

        then LIN (b9,a9,a19) by ANALMETR: 40;

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

        hence contradiction by A2, ANALMETR: 40;

      end;

      then for x9 holds x9 in M9 iff LIN (b9,b19,x9) by A22, A23, A24, AFF_1: 21, AFF_1: 25;

      then M9 = ( Line (b9,b19)) by AFF_1:def 2;

      then A9 // M9 by A14, A28, AFF_1:def 5;

      then (b9,c9) // (b19,c19) by A1, A8, A9, A10, A22, A23, A24, A19, A20, A21, A27, A25, A11, A15;

      hence thesis by ANALMETR: 36;

    end;

    theorem :: CONMETR:9

    X is satisfying_MH1 implies X is satisfying_OSCH

    proof

      assume

       A1: X is satisfying_MH1;

      let a1, a2, a3, a4, b1, b2, b3, b4, M, N;

      assume that

       A2: M _|_ N and

       A3: a1 in M and

       A4: a3 in M and

       A5: b1 in M and

       A6: b3 in M and

       A7: a2 in N and

       A8: a4 in N and

       A9: b2 in N and

       A10: b4 in N and

       A11: not a4 in M and

       A12: not a2 in M and

       A13: not b2 in M and

       A14: not b4 in M and

       A15: not a1 in N and

       A16: not a3 in N and

       A17: not b1 in N and not b3 in N and

       A18: (a3,a2) // (b3,b2) and

       A19: (a2,a1) // (b2,b1) and

       A20: (a1,a4) // (b1,b4);

      reconsider M9 = M, N9 = N as Subset of the AffinStruct of X;

      N is being_line by A2, ANALMETR: 44;

      then

       A21: N9 is being_line by ANALMETR: 43;

      reconsider b49 = b4, b19 = b1, b29 = b2, b39 = b3, a19 = a1, a29 = a2, a39 = a3, a49 = a4 as Element of the AffinStruct of X;

      M is being_line by A2, ANALMETR: 44;

      then

       A22: M9 is being_line by ANALMETR: 43;

       not M9 // N9

      proof

        assume M9 // N9;

        then M // N by ANALMETR: 46;

        hence contradiction by A2, ANALMETR: 52;

      end;

      then ex o9 be Element of the AffinStruct of X st o9 in M9 & o9 in N9 by A22, A21, AFF_1: 58;

      then

      consider o such that

       A23: o in M and

       A24: o in N;

      reconsider o9 = o as Element of the AffinStruct of X;

       A25:

      now

        assume

         A26: b2 <> b4;

         A27:

        now

          consider e19 be Element of the AffinStruct of X such that

           A28: o9 <> e19 and

           A29: e19 in M9 by A22, AFF_1: 20;

          reconsider e1 = e19 as Element of X;

          ex d49 be Element of the AffinStruct of X st o9 <> d49 & d49 in N9 by A21, AFF_1: 20;

          then

          consider d4 such that

           A30: d4 in N and

           A31: d4 <> o;

          reconsider d49 = d4 as Element of the AffinStruct of X;

          consider e2 such that

           A32: (a1,a4) _|_ (d4,e2) and

           A33: e2 <> d4 by ANALMETR: 39;

          reconsider e29 = e2 as Element of the AffinStruct of X;

          assume

           A34: b1 <> b3;

           not (o9,e19) // (d49,e29)

          proof

            

             A35: a49 <> a29

            proof

              assume a49 = a29;

              then (a2,a1) // (b1,b4) by A20, ANALMETR: 59;

              then (b1,b4) // (b2,b1) by A3, A12, A19, ANALMETR: 60;

              then (b1,b4) // (b1,b2) by ANALMETR: 59;

              then LIN (b1,b4,b2) by ANALMETR:def 10;

              then LIN (b19,b49,b29) by ANALMETR: 40;

              then LIN (b29,b49,b19) by AFF_1: 6;

              hence contradiction by A9, A10, A17, A21, A26, AFF_1: 25;

            end;

            

             A36: a1 <> a3

            proof

              assume a1 = a3;

              then (a3,a2) // (b2,b1) by A19, ANALMETR: 59;

              then (b3,b2) // (b2,b1) by A4, A12, A18, ANALMETR: 60;

              then (b2,b3) // (b2,b1) by ANALMETR: 59;

              then LIN (b2,b3,b1) by ANALMETR:def 10;

              then LIN (b29,b39,b19) by ANALMETR: 40;

              then LIN (b19,b39,b29) by AFF_1: 6;

              hence contradiction by A5, A6, A13, A22, A34, AFF_1: 25;

            end;

            assume (o9,e19) // (d49,e29);

            then (o,e1) // (d4,e2) by ANALMETR: 36;

            then

             A37: (o,e1) _|_ (a1,a4) by A32, A33, ANALMETR: 62;

            (o9,e19) // (a19,a39) by A3, A4, A22, A23, A29, AFF_1: 39, AFF_1: 41;

            then (o,e1) // (a1,a3) by ANALMETR: 36;

            then

             A38: (a1,a3) _|_ (a1,a4) by A28, A37, ANALMETR: 62;

            (a1,a3) _|_ (a2,a4) by A2, A3, A4, A7, A8, ANALMETR: 56;

            then (a1,a4) // (a2,a4) by A38, A36, ANALMETR: 63;

            then (a4,a2) // (a4,a1) by ANALMETR: 59;

            then LIN (a4,a2,a1) by ANALMETR:def 10;

            then LIN (a49,a29,a19) by ANALMETR: 40;

            hence contradiction by A7, A8, A15, A21, A35, AFF_1: 25;

          end;

          then

          consider d19 be Element of the AffinStruct of X such that

           A39: LIN (o9,e19,d19) and

           A40: LIN (d49,e29,d19) by AFF_1: 60;

          reconsider d1 = d19 as Element of X;

          consider e19 be Element of the AffinStruct of X such that

           A41: o9 <> e19 and

           A42: e19 in N9 by A21, AFF_1: 20;

          

           A43: d1 in M by A22, A23, A28, A29, A39, AFF_1: 25;

           LIN (d4,e2,d1) by A40, ANALMETR: 40;

          then (d4,e2) // (d4,d1) by ANALMETR:def 10;

          then

           A44: (d1,d4) // (d4,e2) by ANALMETR: 59;

          then (a1,a4) _|_ (d1,d4) by A32, A33, ANALMETR: 62;

          then

           A45: (b1,b4) _|_ (d1,d4) by A3, A11, A20, ANALMETR: 62;

          reconsider e1 = e19 as Element of X;

          consider e2 such that

           A46: (a2,a1) _|_ (d1,e2) and

           A47: e2 <> d1 by ANALMETR: 39;

          reconsider e29 = e2 as Element of the AffinStruct of X;

           not (o9,e19) // (e29,d19)

          proof

            

             A48: a19 <> a39

            proof

              assume a19 = a39;

              then (a3,a2) // (b2,b1) by A19, ANALMETR: 59;

              then (b3,b2) // (b2,b1) by A4, A12, A18, ANALMETR: 60;

              then (b2,b3) // (b2,b1) by ANALMETR: 59;

              then LIN (b2,b3,b1) by ANALMETR:def 10;

              then LIN (b29,b39,b19) by ANALMETR: 40;

              then LIN (b19,b39,b29) by AFF_1: 6;

              hence contradiction by A5, A6, A13, A22, A34, AFF_1: 25;

            end;

            (o9,e19) // (a29,a49) by A7, A8, A21, A24, A42, AFF_1: 39, AFF_1: 41;

            then

             A49: (o,e1) // (a2,a4) by ANALMETR: 36;

            

             A50: a2 <> a4

            proof

              assume a2 = a4;

              then (a2,a1) // (b1,b4) by A20, ANALMETR: 59;

              then (b1,b4) // (b2,b1) by A3, A12, A19, ANALMETR: 60;

              then (b1,b4) // (b1,b2) by ANALMETR: 59;

              then LIN (b1,b4,b2) by ANALMETR:def 10;

              then LIN (b19,b49,b29) by ANALMETR: 40;

              then LIN (b29,b49,b19) by AFF_1: 6;

              hence contradiction by A9, A10, A17, A21, A26, AFF_1: 25;

            end;

            assume (o9,e19) // (e29,d19);

            then

             A51: (o,e1) // (e2,d1) by ANALMETR: 36;

            (a2,a1) _|_ (e2,d1) by A46, ANALMETR: 61;

            then (o,e1) _|_ (a2,a1) by A47, A51, ANALMETR: 62;

            then

             A52: (a2,a1) _|_ (a2,a4) by A41, A49, ANALMETR: 62;

            (a3,a1) _|_ (a2,a4) by A2, A3, A4, A7, A8, ANALMETR: 56;

            then (a3,a1) // (a2,a1) by A52, A50, ANALMETR: 63;

            then (a1,a3) // (a1,a2) by ANALMETR: 59;

            then LIN (a1,a3,a2) by ANALMETR:def 10;

            then LIN (a19,a39,a29) by ANALMETR: 40;

            hence contradiction by A3, A4, A12, A22, A48, AFF_1: 25;

          end;

          then

          consider d29 be Element of the AffinStruct of X such that

           A53: LIN (o9,e19,d29) and

           A54: LIN (e29,d19,d29) by AFF_1: 60;

          reconsider d2 = d29 as Element of X;

          

           A55: d2 in N by A21, A24, A41, A42, A53, AFF_1: 25;

           LIN (d19,d29,e29) by A54, AFF_1: 6;

          then LIN (d1,d2,e2) by ANALMETR: 40;

          then (d1,d2) // (d1,e2) by ANALMETR:def 10;

          then

           A56: (d2,d1) // (e2,d1) by ANALMETR: 59;

          

           A57: (a2,a1) _|_ (e2,d1) by A46, ANALMETR: 61;

          then

           A58: (a2,a1) _|_ (d2,d1) by A47, A56, ANALMETR: 62;

          consider e19 be Element of the AffinStruct of X such that

           A59: o9 <> e19 and

           A60: e19 in M9 by A22, AFF_1: 20;

          reconsider e1 = e19 as Element of X;

          consider e2 such that

           A61: (a3,a2) _|_ (d2,e2) and

           A62: e2 <> d2 by ANALMETR: 39;

          reconsider e29 = e2 as Element of the AffinStruct of X;

           not (o9,e19) // (e29,d29)

          proof

            

             A63: a29 <> a49

            proof

              assume a29 = a49;

              then (a2,a1) // (b1,b4) by A20, ANALMETR: 59;

              then (b1,b4) // (b2,b1) by A3, A12, A19, ANALMETR: 60;

              then (b1,b4) // (b1,b2) by ANALMETR: 59;

              then LIN (b1,b4,b2) by ANALMETR:def 10;

              then LIN (b19,b49,b29) by ANALMETR: 40;

              then LIN (b29,b49,b19) by AFF_1: 6;

              hence contradiction by A9, A10, A17, A21, A26, AFF_1: 25;

            end;

            assume (o9,e19) // (e29,d29);

            then (o,e1) // (e2,d2) by ANALMETR: 36;

            then (o,e1) // (d2,e2) by ANALMETR: 59;

            then

             A64: (a3,a2) _|_ (o,e1) by A61, A62, ANALMETR: 62;

            (o,e1) _|_ (a2,a4) by A2, A7, A8, A23, A60, ANALMETR: 56;

            then (a3,a2) // (a2,a4) by A59, A64, ANALMETR: 63;

            then (a2,a4) // (a2,a3) by ANALMETR: 59;

            then LIN (a2,a4,a3) by ANALMETR:def 10;

            then LIN (a29,a49,a39) by ANALMETR: 40;

            hence contradiction by A7, A8, A16, A21, A63, AFF_1: 25;

          end;

          then

          consider d39 be Element of the AffinStruct of X such that

           A65: LIN (o9,e19,d39) and

           A66: LIN (e29,d29,d39) by AFF_1: 60;

          reconsider d3 = d39 as Element of X;

          

           A67: d3 in M by A22, A23, A59, A60, A65, AFF_1: 25;

          then

           A68: d3 <> d4 by A2, A22, A21, A23, A24, A30, A31, AFF_1: 18;

          (a2,a1) _|_ (d2,d1) by A47, A56, A57, ANALMETR: 62;

          then

           A69: (b2,b1) _|_ (d2,d1) by A3, A12, A19, ANALMETR: 62;

           LIN (d29,d39,e29) by A66, AFF_1: 6;

          then LIN (d2,d3,e2) by ANALMETR: 40;

          then (d2,d3) // (d2,e2) by ANALMETR:def 10;

          then (d3,d2) // (d2,e2) by ANALMETR: 59;

          then

           A70: (a3,a2) _|_ (d3,d2) by A61, A62, ANALMETR: 62;

          then (b3,b2) _|_ (d3,d2) by A4, A12, A18, ANALMETR: 62;

          then

           A71: (b3,b4) _|_ (d3,d4) by A1, A2, A5, A6, A9, A10, A13, A14, A30, A43, A55, A67, A45, A69;

          (a1,a4) _|_ (d1,d4) by A32, A33, A44, ANALMETR: 62;

          then (a3,a4) _|_ (d3,d4) by A1, A2, A3, A4, A7, A8, A11, A12, A30, A43, A55, A58, A70, A67;

          hence thesis by A68, A71, ANALMETR: 63;

        end;

        now

          

           A72: not LIN (o9,a29,a19) by A7, A12, A15, A21, A23, A24, AFF_1: 48, AFF_1:def 1;

          

           A73: LIN (o9,a19,a39) by A3, A4, A22, A23, AFF_1: 21;

          assume

           A74: b1 = b3;

          then (a2,a3) // (b2,b1) by A18, ANALMETR: 59;

          then

           A75: (a29,a39) // (b29,b19) by ANALMETR: 36;

          (a29,a19) // (b29,b19) by A19, ANALMETR: 36;

          then (a29,a19) // (a29,a39) by A5, A13, A75, AFF_1: 5;

          hence thesis by A20, A74, A72, A73, AFF_1: 14;

        end;

        hence thesis by A27;

      end;

      now

        

         A76: not LIN (o9,a19,a49)

        proof

          assume LIN (o9,a19,a49);

          then ex A9 st A9 is being_line & o9 in A9 & a19 in A9 & a49 in A9 by AFF_1: 21;

          hence contradiction by A3, A11, A15, A22, A23, A24, AFF_1: 18;

        end;

        assume

         A77: b2 = b4;

        (b1,b2) // (a1,a2) by A19, ANALMETR: 59;

        then (a1,a4) // (a1,a2) by A5, A13, A20, A77, ANALMETR: 60;

        then

         A78: (a19,a49) // (a19,a29) by ANALMETR: 36;

         LIN (o9,a49,a29) by A7, A8, A21, A24, AFF_1: 21;

        hence thesis by A18, A77, A78, A76, AFF_1: 14;

      end;

      hence thesis by A25;

    end;

    theorem :: CONMETR:10

    X is satisfying_MH2 implies X is satisfying_OSCH

    proof

      assume

       A1: X is satisfying_MH2;

      let a1, a2, a3, a4, b1, b2, b3, b4, M, N;

      assume that

       A2: M _|_ N and

       A3: a1 in M and

       A4: a3 in M and

       A5: b1 in M and

       A6: b3 in M and

       A7: a2 in N and

       A8: a4 in N and

       A9: b2 in N and

       A10: b4 in N and

       A11: not a4 in M and

       A12: not a2 in M and

       A13: not b2 in M and

       A14: not b4 in M and

       A15: not a1 in N and

       A16: not a3 in N and

       A17: not b1 in N and not b3 in N and

       A18: (a3,a2) // (b3,b2) and

       A19: (a2,a1) // (b2,b1) and

       A20: (a1,a4) // (b1,b4);

      reconsider M9 = M, N9 = N as Subset of the AffinStruct of X;

      N is being_line by A2, ANALMETR: 44;

      then

       A21: N9 is being_line by ANALMETR: 43;

      reconsider b49 = b4, b19 = b1, b29 = b2, b39 = b3, a19 = a1, a29 = a2, a39 = a3, a49 = a4 as Element of the AffinStruct of X;

      M is being_line by A2, ANALMETR: 44;

      then

       A22: M9 is being_line by ANALMETR: 43;

       not M9 // N9

      proof

        assume M9 // N9;

        then M // N by ANALMETR: 46;

        hence contradiction by A2, ANALMETR: 52;

      end;

      then ex o9 be Element of the AffinStruct of X st o9 in M9 & o9 in N9 by A22, A21, AFF_1: 58;

      then

      consider o such that

       A23: o in M and

       A24: o in N;

      reconsider o9 = o as Element of the AffinStruct of X;

       A25:

      now

        assume

         A26: b2 <> b4;

         A27:

        now

          ex d39 be Element of the AffinStruct of X st o9 <> d39 & d39 in N9 by A21, AFF_1: 20;

          then

          consider d3 such that

           A28: d3 in N and

           A29: d3 <> o;

          reconsider d39 = d3 as Element of the AffinStruct of X;

          consider e2 such that

           A30: (a3,a2) _|_ (d3,e2) and

           A31: d3 <> e2 by ANALMETR:def 9;

          consider e1 such that

           A32: (a3,a1) // (a3,e1) and

           A33: a3 <> e1 by ANALMETR: 39;

          reconsider e19 = e1, e29 = e2 as Element of the AffinStruct of X;

          assume

           A34: b1 <> b3;

          

           A35: a1 <> a3 & a2 <> a4

          proof

            assume a1 = a3 or a2 = a4;

            then (a2,a1) // (b3,b2) or (a1,a4) // (b2,b1) by A18, A19, ANALMETR: 59;

            then (b3,b2) // (b2,b1) or (b2,b1) // (b1,b4) by A3, A11, A12, A19, A20, ANALMETR: 60;

            then (b2,b3) // (b2,b1) or (b1,b2) // (b1,b4) by ANALMETR: 59;

            then LIN (b2,b3,b1) or LIN (b1,b2,b4) by ANALMETR:def 10;

            then LIN (b29,b39,b19) or LIN (b19,b29,b49) by ANALMETR: 40;

            then LIN (b19,b39,b29) or LIN (b29,b49,b19) by AFF_1: 6;

            hence contradiction by A5, A6, A9, A10, A13, A17, A22, A21, A26, A34, AFF_1: 25;

          end;

           not (a39,e19) // (d39,e29)

          proof

            assume (a39,e19) // (d39,e29);

            then (a3,e1) // (d3,e2) by ANALMETR: 36;

            then (a3,a1) // (d3,e2) by A32, A33, ANALMETR: 60;

            then

             A36: (a3,a2) _|_ (a3,a1) by A30, A31, ANALMETR: 62;

            (a3,a1) _|_ (a2,a4) by A2, A3, A4, A7, A8, ANALMETR: 56;

            then (a3,a2) // (a2,a4) by A35, A36, ANALMETR: 63;

            then (a2,a4) // (a2,a3) by ANALMETR: 59;

            then LIN (a2,a4,a3) by ANALMETR:def 10;

            then LIN (a29,a49,a39) by ANALMETR: 40;

            hence contradiction by A7, A8, A16, A21, A35, AFF_1: 25;

          end;

          then

          consider d29 be Element of the AffinStruct of X such that

           A37: LIN (a39,e19,d29) and

           A38: LIN (d39,e29,d29) by AFF_1: 60;

          reconsider d2 = d29 as Element of X;

           LIN (d3,e2,d2) by A38, ANALMETR: 40;

          then (d3,e2) // (d3,d2) by ANALMETR:def 10;

          then

           A39: (a3,a2) _|_ (d3,d2) by A30, A31, ANALMETR: 62;

           LIN (a3,e1,d2) by A37, ANALMETR: 40;

          then (a3,e1) // (a3,d2) by ANALMETR:def 10;

          then (a3,a1) // (a3,d2) by A32, A33, ANALMETR: 60;

          then LIN (a3,a1,d2) by ANALMETR:def 10;

          then LIN (a39,a19,d29) by ANALMETR: 40;

          then

          consider d2 such that

           A40: d2 in M and

           A41: (a3,a2) _|_ (d3,d2) by A3, A4, A22, A35, A39, AFF_1: 25;

          reconsider d29 = d2 as Element of the AffinStruct of X;

          consider e1 such that

           A42: (a2,a4) // (a2,e1) and

           A43: a2 <> e1 by ANALMETR: 39;

          consider e2 such that

           A44: (a2,a1) _|_ (d2,e2) and

           A45: d2 <> e2 by ANALMETR:def 9;

          reconsider e19 = e1, e29 = e2 as Element of the AffinStruct of X;

           not (a29,e19) // (d29,e29)

          proof

            assume (a29,e19) // (d29,e29);

            then (a2,e1) // (d2,e2) by ANALMETR: 36;

            then (a2,a4) // (d2,e2) by A42, A43, ANALMETR: 60;

            then

             A46: (a2,a4) _|_ (a2,a1) by A44, A45, ANALMETR: 62;

            (a1,a3) _|_ (a2,a4) by A2, A3, A4, A7, A8, ANALMETR: 56;

            then (a1,a3) // (a2,a1) by A35, A46, ANALMETR: 63;

            then (a1,a3) // (a1,a2) by ANALMETR: 59;

            then LIN (a1,a3,a2) by ANALMETR:def 10;

            then LIN (a19,a39,a29) by ANALMETR: 40;

            hence contradiction by A3, A4, A12, A22, A35, AFF_1: 25;

          end;

          then

          consider d19 be Element of the AffinStruct of X such that

           A47: LIN (a29,e19,d19) and

           A48: LIN (d29,e29,d19) by AFF_1: 60;

          reconsider d1 = d19 as Element of X;

          

           A49: (b3,b2) _|_ (d3,d2) by A4, A12, A18, A41, ANALMETR: 62;

           LIN (a2,e1,d1) by A47, ANALMETR: 40;

          then (a2,e1) // (a2,d1) by ANALMETR:def 10;

          then (a2,a4) // (a2,d1) by A42, A43, ANALMETR: 60;

          then LIN (a2,a4,d1) by ANALMETR:def 10;

          then LIN (a29,a49,d19) by ANALMETR: 40;

          then

           A50: d1 in N by A7, A8, A21, A35, AFF_1: 25;

           LIN (d2,e2,d1) by A48, ANALMETR: 40;

          then (d2,e2) // (d2,d1) by ANALMETR:def 10;

          then

           A51: (a2,a1) _|_ (d2,d1) by A44, A45, ANALMETR: 62;

          then

           A52: (b2,b1) _|_ (d2,d1) by A3, A12, A19, ANALMETR: 62;

          consider e2 such that

           A53: (a1,a4) _|_ (d1,e2) and

           A54: d1 <> e2 by ANALMETR: 39;

          consider e1 such that

           A55: (a1,a3) // (a1,e1) and

           A56: a1 <> e1 by ANALMETR: 39;

          reconsider e19 = e1, e29 = e2 as Element of the AffinStruct of X;

           not (a19,e19) // (d19,e29)

          proof

            assume (a19,e19) // (d19,e29);

            then (a1,e1) // (d1,e2) by ANALMETR: 36;

            then (a1,a3) // (d1,e2) by A55, A56, ANALMETR: 60;

            then

             A57: (a1,a3) _|_ (a1,a4) by A53, A54, ANALMETR: 62;

            (a1,a3) _|_ (a2,a4) by A2, A3, A4, A7, A8, ANALMETR: 56;

            then (a2,a4) // (a1,a4) by A35, A57, ANALMETR: 63;

            then (a4,a2) // (a4,a1) by ANALMETR: 59;

            then LIN (a4,a2,a1) by ANALMETR:def 10;

            then LIN (a49,a29,a19) by ANALMETR: 40;

            hence contradiction by A7, A8, A15, A21, A35, AFF_1: 25;

          end;

          then

          consider d49 be Element of the AffinStruct of X such that

           A58: LIN (a19,e19,d49) and

           A59: LIN (d19,e29,d49) by AFF_1: 60;

          reconsider d4 = d49 as Element of X;

           LIN (a1,e1,d4) by A58, ANALMETR: 40;

          then (a1,e1) // (a1,d4) by ANALMETR:def 10;

          then (a1,a3) // (a1,d4) by A55, A56, ANALMETR: 60;

          then LIN (a1,a3,d4) by ANALMETR:def 10;

          then LIN (a19,a39,d49) by ANALMETR: 40;

          then

           A60: d4 in M by A3, A4, A22, A35, AFF_1: 25;

          then

           A61: d3 <> d4 by A2, A22, A21, A23, A24, A28, A29, AFF_1: 18;

           LIN (d1,e2,d4) by A59, ANALMETR: 40;

          then (d1,e2) // (d1,d4) by ANALMETR:def 10;

          then

           A62: (a1,a4) _|_ (d1,d4) by A53, A54, ANALMETR: 62;

          then (b1,b4) _|_ (d1,d4) by A3, A11, A20, ANALMETR: 62;

          then

           A63: (b3,b4) _|_ (d3,d4) by A1, A2, A5, A6, A9, A10, A13, A14, A28, A40, A50, A60, A49, A52;

          (a3,a4) _|_ (d3,d4) by A1, A2, A3, A4, A7, A8, A11, A12, A28, A40, A41, A50, A51, A60, A62;

          hence thesis by A63, A61, ANALMETR: 63;

        end;

        now

          (o9,a19) // (o9,a39) by A3, A4, A22, A23, AFF_1: 39, AFF_1: 41;

          then

           A64: LIN (o9,a19,a39) by AFF_1:def 1;

          assume

           A65: b1 = b3;

          then (a2,a1) // (b3,b2) by A19, ANALMETR: 59;

          then (a2,a1) // (a3,a2) by A6, A13, A18, ANALMETR: 60;

          then (a2,a1) // (a2,a3) by ANALMETR: 59;

          then (a29,a19) // (a29,a39) by ANALMETR: 36;

          hence thesis by A7, A12, A15, A20, A21, A23, A24, A65, A64, AFF_1: 14, AFF_1: 25;

        end;

        hence thesis by A27;

      end;

      now

        (o9,a29) // (o9,a49) by A7, A8, A21, A24, AFF_1: 39, AFF_1: 41;

        then

         A66: LIN (o9,a29,a49) by AFF_1:def 1;

        assume

         A67: b2 = b4;

        then (a1,a4) // (b2,b1) by A20, ANALMETR: 59;

        then (a2,a1) // (a1,a4) by A5, A13, A19, ANALMETR: 60;

        then (a1,a2) // (a1,a4) by ANALMETR: 59;

        then (a19,a29) // (a19,a49) by ANALMETR: 36;

        hence thesis by A3, A12, A15, A18, A22, A23, A24, A67, A66, AFF_1: 14, AFF_1: 25;

      end;

      hence thesis by A25;

    end;

    theorem :: CONMETR:11

    X is satisfying_AH implies X is satisfying_TDES

    proof

      assume

       A1: X is satisfying_AH;

      let o, a, a1, b, b1, c, c1;

      assume that

       A2: o <> a and

       A3: o <> a1 and

       A4: o <> b and

       A5: o <> b1 and

       A6: o <> c and

       A7: o <> c1 and

       A8: not LIN (b,b1,a) and

       A9: not LIN (b,b1,c) and

       A10: LIN (o,a,a1) and

       A11: LIN (o,b,b1) and

       A12: LIN (o,c,c1) and

       A13: (a,b) // (a1,b1) and

       A14: (a,b) // (o,c) and

       A15: (b,c) // (b1,c1);

      consider e1 such that

       A16: (o,b) _|_ (o,e1) and

       A17: o <> e1 by ANALMETR:def 9;

      consider c2 such that

       A18: (o,c) _|_ (o,c2) and

       A19: o <> c2 by ANALMETR:def 9;

      consider e2 such that

       A20: (b,c) _|_ (c2,e2) and

       A21: c2 <> e2 by ANALMETR:def 9;

      reconsider o9 = o, a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1, c29 = c2, e19 = e1, e29 = e2 as Element of the AffinStruct of X;

      

       A22: b1 <> a1

      proof

        assume b1 = a1;

        then LIN (o9,b9,a19) by A11, ANALMETR: 40;

        then (o9,b9) // (o9,a19) by AFF_1:def 1;

        then (o9,a19) // (o9,b9) by AFF_1: 4;

        then

         A23: (o,a1) // (o,b) by ANALMETR: 36;

        (o,a) // (o,a1) by A10, ANALMETR:def 10;

        then (o9,a9) // (o9,a19) by ANALMETR: 36;

        then (o9,a19) // (o9,a9) by AFF_1: 4;

        then (o,a1) // (o,a) by ANALMETR: 36;

        then (o,a) // (o,b) by A3, A23, ANALMETR: 60;

        then LIN (o,a,b) by ANALMETR:def 10;

        then

         A24: LIN (o9,a9,b9) by ANALMETR: 40;

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

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

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

        then

         A25: (o,b) // (a,b) by ANALMETR: 36;

        

         A26: a9 <> b9

        proof

          assume a9 = b9;

          then LIN (b9,b19,a9) by AFF_1: 7;

          hence contradiction by A8, ANALMETR: 40;

        end;

        (o,b) // (o,b1) by A11, ANALMETR:def 10;

        then (a,b) // (o,b1) by A4, A25, ANALMETR: 60;

        then

         A27: (a9,b9) // (o9,b19) by ANALMETR: 36;

         LIN (a9,b9,o9) by A24, AFF_1: 6;

        then LIN (a9,b9,b19) by A27, A26, AFF_1: 9;

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

        hence contradiction by A8, ANALMETR: 40;

      end;

       A28:

      now

         not (o9,e19) // (c29,e29)

        proof

          assume (o9,e19) // (c29,e29);

          then (o,e1) // (c2,e2) by ANALMETR: 36;

          then (c2,e2) _|_ (o,b) by A16, A17, ANALMETR: 62;

          then (c2,e2) _|_ (b,o) by ANALMETR: 61;

          then (b,c) // (b,o) by A20, A21, ANALMETR: 63;

          then LIN (b,c,o) by ANALMETR:def 10;

          then LIN (b9,c9,o9) by ANALMETR: 40;

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

          then LIN (b,o,c) by ANALMETR: 40;

          then

           A29: (b,o) // (b,c) by ANALMETR:def 10;

           LIN (o9,b9,b19) by A11, ANALMETR: 40;

          then LIN (b9,o9,b19) by AFF_1: 6;

          then LIN (b,o,b1) by ANALMETR: 40;

          then (b,o) // (b,b1) by ANALMETR:def 10;

          then (b,b1) // (b,c) by A4, A29, ANALMETR: 60;

          hence contradiction by A9, ANALMETR:def 10;

        end;

        then

        consider b29 such that

         A30: LIN (o9,e19,b29) and

         A31: LIN (c29,e29,b29) by AFF_1: 60;

        reconsider b2 = b29 as Element of X;

         LIN (o,e1,b2) by A30, ANALMETR: 40;

        then (o,e1) // (o,b2) by ANALMETR:def 10;

        then

         A32: (o,b) _|_ (o,b2) by A16, A17, ANALMETR: 62;

        (o,b) // (o,b1) by A11, ANALMETR:def 10;

        then

         A33: (o,b1) _|_ (o,b2) by A4, A32, ANALMETR: 62;

        assume

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

        

         A35: b <> a

        proof

          assume b = a;

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

          hence contradiction by A34, ANALMETR: 40;

        end;

        

         A36: not (o,c) // (o,b)

        proof

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

          then LIN (o,c,b) by ANALMETR:def 10;

          then LIN (o9,c9,b9) by ANALMETR: 40;

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

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

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

          then

           A37: (o,c) // (b,c) by ANALMETR: 36;

          (a9,b9) // (o9,c9) by A14, ANALMETR: 36;

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

          then (o,c) // (b,a) by ANALMETR: 36;

          then (b,a) // (b,c) by A6, A37, ANALMETR: 60;

          then LIN (b,a,c) by ANALMETR:def 10;

          then LIN (b9,a9,c9) by ANALMETR: 40;

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

          hence contradiction by A34, ANALMETR: 40;

        end;

        

         A38: not (o,a) // (o,c)

        proof

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

          then LIN (o,a,c) by ANALMETR:def 10;

          then LIN (o9,a9,c9) by ANALMETR: 40;

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

          then LIN (c,o,a) by ANALMETR: 40;

          then

           A39: (c,o) // (c,a) by ANALMETR:def 10;

          (a9,b9) // (o9,c9) by A14, ANALMETR: 36;

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

          then (c,o) // (a,b) by ANALMETR: 36;

          then (a,b) // (c,a) by A6, A39, ANALMETR: 60;

          then (a9,b9) // (c9,a9) by ANALMETR: 36;

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

          then (a,b) // (a,c) by ANALMETR: 36;

          hence contradiction by A34, ANALMETR:def 10;

        end;

         LIN (c2,e2,b2) by A31, ANALMETR: 40;

        then (c2,e2) // (c2,b2) by ANALMETR:def 10;

        then

         A40: (b,c) _|_ (c2,b2) by A20, A21, ANALMETR: 62;

        consider e1 such that

         A41: (o,a) _|_ (o,e1) and

         A42: o <> e1 by ANALMETR:def 9;

        consider e2 such that

         A43: (a,c) _|_ (c2,e2) and

         A44: c2 <> e2 by ANALMETR:def 9;

        reconsider e19 = e1, e29 = e2 as Element of the AffinStruct of X;

         not (o9,e19) // (c29,e29)

        proof

          assume (o9,e19) // (c29,e29);

          then (o,e1) // (c2,e2) by ANALMETR: 36;

          then (c2,e2) _|_ (o,a) by A41, A42, ANALMETR: 62;

          then (a,c) // (o,a) by A43, A44, ANALMETR: 63;

          then (a9,c9) // (o9,a9) by ANALMETR: 36;

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

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

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

          then LIN (c,o,a) by ANALMETR: 40;

          then

           A45: (c,o) // (c,a) by ANALMETR:def 10;

          (a9,b9) // (o9,c9) by A14, ANALMETR: 36;

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

          then (c,o) // (a,b) by ANALMETR: 36;

          then (a,b) // (c,a) by A6, A45, ANALMETR: 60;

          then (a9,b9) // (c9,a9) by ANALMETR: 36;

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

          then (a,b) // (a,c) by ANALMETR: 36;

          hence contradiction by A34, ANALMETR:def 10;

        end;

        then

        consider a29 such that

         A46: LIN (o9,e19,a29) and

         A47: LIN (c29,e29,a29) by AFF_1: 60;

        reconsider a2 = a29 as Element of X;

         LIN (o,e1,a2) by A46, ANALMETR: 40;

        then (o,e1) // (o,a2) by ANALMETR:def 10;

        then

         A48: (o,a) _|_ (o,a2) by A41, A42, ANALMETR: 62;

        

         A49: c2 <> a2

        proof

          assume c2 = a2;

          then (o,c) // (o,a) by A18, A19, A48, ANALMETR: 63;

          then LIN (o,c,a) by ANALMETR:def 10;

          then LIN (o9,c9,a9) by ANALMETR: 40;

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

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

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

          then (o,c) // (a,c) by ANALMETR: 36;

          then (a,b) // (a,c) by A6, A14, ANALMETR: 60;

          hence contradiction by A34, ANALMETR:def 10;

        end;

         LIN (c2,e2,a2) by A47, ANALMETR: 40;

        then (c2,e2) // (c2,a2) by ANALMETR:def 10;

        then (a,c) _|_ (c2,a2) by A43, A44, ANALMETR: 62;

        then

         A50: (c,a) _|_ (c2,a2) by ANALMETR: 61;

        

         A51: not LIN (o9,b29,a29)

        proof

          

           A52: o <> b2

          proof

            (a9,b9) // (o9,c9) by A14, ANALMETR: 36;

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

            then

             A53: (o,c) // (b,a) by ANALMETR: 36;

            assume o = b2;

            then (o,c2) _|_ (b,c) by A40, ANALMETR: 61;

            then (o,c) // (b,c) by A18, A19, ANALMETR: 63;

            then (b,a) // (b,c) by A6, A53, ANALMETR: 60;

            then LIN (b,a,c) by ANALMETR:def 10;

            then LIN (b9,a9,c9) by ANALMETR: 40;

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

            hence contradiction by A34, ANALMETR: 40;

          end;

          

           A54: o <> a2

          proof

            assume

             A55: o = a2;

            (c2,o) _|_ (o,c) by A18, ANALMETR: 61;

            then (o,c) // (c,a) by A19, A50, A55, ANALMETR: 63;

            then (a,b) // (c,a) by A6, A14, ANALMETR: 60;

            then (a9,b9) // (c9,a9) by ANALMETR: 36;

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

            then (a,b) // (a,c) by ANALMETR: 36;

            hence contradiction by A34, ANALMETR:def 10;

          end;

          assume LIN (o9,b29,a29);

          then LIN (o,b2,a2) by ANALMETR: 40;

          then (o,b2) // (o,a2) by ANALMETR:def 10;

          then (o,a2) _|_ (o,b) by A32, A52, ANALMETR: 62;

          then (o,a) // (o,b) by A48, A54, ANALMETR: 63;

          then LIN (o,a,b) by ANALMETR:def 10;

          then LIN (o9,a9,b9) by ANALMETR: 40;

          then

           A56: LIN (a9,b9,o9) by AFF_1: 6;

          

           A57: a9 <> b9

          proof

            assume a9 = b9;

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

            hence contradiction by A34, ANALMETR: 40;

          end;

          (a9,b9) // (o9,c9) by A14, ANALMETR: 36;

          then LIN (a9,b9,c9) by A56, A57, AFF_1: 9;

          hence contradiction by A34, ANALMETR: 40;

        end;

        consider e1 such that

         A58: (o,a1) _|_ (o,e1) and

         A59: o <> e1 by ANALMETR:def 9;

        consider e2 such that

         A60: (a1,c1) _|_ (c2,e2) and

         A61: c2 <> e2 by ANALMETR:def 9;

        reconsider e19 = e1, e29 = e2 as Element of the AffinStruct of X;

         not (o9,e19) // (c29,e29)

        proof

          assume (o9,e19) // (c29,e29);

          then (o,e1) // (c2,e2) by ANALMETR: 36;

          then (c2,e2) _|_ (o,a1) by A58, A59, ANALMETR: 62;

          then (a1,c1) // (o,a1) by A60, A61, ANALMETR: 63;

          then (a19,c19) // (o9,a19) by ANALMETR: 36;

          then (a19,c19) // (a19,o9) by AFF_1: 4;

          then LIN (a19,c19,o9) by AFF_1:def 1;

          then LIN (o9,c19,a19) by AFF_1: 6;

          then (o9,c19) // (o9,a19) by AFF_1:def 1;

          then

           A62: (o,c1) // (o,a1) by ANALMETR: 36;

           LIN (o9,a9,a19) by A10, ANALMETR: 40;

          then (o9,a9) // (o9,a19) by AFF_1:def 1;

          then (o9,a19) // (o9,a9) by AFF_1: 4;

          then

           A63: (o,a1) // (o,a) by ANALMETR: 36;

           LIN (o9,c9,c19) by A12, ANALMETR: 40;

          then (o9,c9) // (o9,c19) by AFF_1:def 1;

          then (o9,c19) // (o9,c9) by AFF_1: 4;

          then (o,c1) // (o,c) by ANALMETR: 36;

          then (o,a1) // (o,c) by A7, A62, ANALMETR: 60;

          then (o,a) // (o,c) by A3, A63, ANALMETR: 60;

          then LIN (o,a,c) by ANALMETR:def 10;

          then LIN (o9,a9,c9) by ANALMETR: 40;

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

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

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

          then (o,c) // (a,c) by ANALMETR: 36;

          then (a,b) // (a,c) by A6, A14, ANALMETR: 60;

          hence contradiction by A34, ANALMETR:def 10;

        end;

        then

        consider a39 such that

         A64: LIN (o9,e19,a39) and

         A65: LIN (c29,e29,a39) by AFF_1: 60;

        reconsider a3 = a39 as Element of X;

         LIN (o,e1,a3) by A64, ANALMETR: 40;

        then (o,e1) // (o,a3) by ANALMETR:def 10;

        then

         A66: (o,a1) _|_ (o,a3) by A58, A59, ANALMETR: 62;

        b <> c

        proof

          assume b = c;

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

          hence contradiction by A34, ANALMETR: 40;

        end;

        then (c2,b2) _|_ (b1,c1) by A15, A40, ANALMETR: 62;

        then

         A67: (c1,b1) _|_ (c2,b2) by ANALMETR: 61;

        

         A68: not (o,a1) // (o,c1)

        proof

          (o,a) // (o,a1) by A10, ANALMETR:def 10;

          then (o9,a9) // (o9,a19) by ANALMETR: 36;

          then (o9,a19) // (o9,a9) by AFF_1: 4;

          then

           A69: (o,a1) // (o,a) by ANALMETR: 36;

          assume (o,a1) // (o,c1);

          then (o9,a19) // (o9,c19) by ANALMETR: 36;

          then (o9,c19) // (o9,a19) by AFF_1: 4;

          then

           A70: (o,c1) // (o,a1) by ANALMETR: 36;

          (o,c) // (o,c1) by A12, ANALMETR:def 10;

          then (o9,c9) // (o9,c19) by ANALMETR: 36;

          then (o9,c19) // (o9,c9) by AFF_1: 4;

          then (o,c1) // (o,c) by ANALMETR: 36;

          then (o,a1) // (o,c) by A7, A70, ANALMETR: 60;

          then (o,a) // (o,c) by A3, A69, ANALMETR: 60;

          then LIN (o,a,c) by ANALMETR:def 10;

          then LIN (o9,a9,c9) by ANALMETR: 40;

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

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

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

          then (o,c) // (a,c) by ANALMETR: 36;

          then (a,b) // (a,c) by A6, A14, ANALMETR: 60;

          hence contradiction by A34, ANALMETR:def 10;

        end;

        (a9,b9) // (o9,c9) by A14, ANALMETR: 36;

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

        then

         A71: (o,c) // (b,a) by ANALMETR: 36;

        

         A72: not (o,c1) // (o,b1)

        proof

          (o,b) // (o,b1) by A11, ANALMETR:def 10;

          then (o9,b9) // (o9,b19) by ANALMETR: 36;

          then (o9,b19) // (o9,b9) by AFF_1: 4;

          then

           A73: (o,b1) // (o,b) by ANALMETR: 36;

          (o,c) // (o,c1) by A12, ANALMETR:def 10;

          then (o9,c9) // (o9,c19) by ANALMETR: 36;

          then (o9,c19) // (o9,c9) by AFF_1: 4;

          then

           A74: (o,c1) // (o,c) by ANALMETR: 36;

          assume (o,c1) // (o,b1);

          then (o,b1) // (o,c) by A7, A74, ANALMETR: 60;

          then (o,b) // (o,c) by A5, A73, ANALMETR: 60;

          then LIN (o,b,c) by ANALMETR:def 10;

          then LIN (o9,b9,c9) by ANALMETR: 40;

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

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

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

          then

           A75: (o,c) // (b,c) by ANALMETR: 36;

          (a9,b9) // (o9,c9) by A14, ANALMETR: 36;

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

          then (o,c) // (b,a) by ANALMETR: 36;

          then (b,a) // (b,c) by A6, A75, ANALMETR: 60;

          then LIN (b,a,c) by ANALMETR:def 10;

          then LIN (b9,a9,c9) by ANALMETR: 40;

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

          hence contradiction by A34, ANALMETR: 40;

        end;

        a <> b

        proof

          assume a = b;

          then LIN (b9,b19,a9) by AFF_1: 7;

          hence contradiction by A8, ANALMETR: 40;

        end;

        then (o,c) // (a1,b1) by A13, A14, ANALMETR: 60;

        then (o9,c9) // (a19,b19) by ANALMETR: 36;

        then (o9,c9) // (b19,a19) by AFF_1: 4;

        then

         A76: (o,c) // (b1,a1) by ANALMETR: 36;

        (o,c) // (o,c1) by A12, ANALMETR:def 10;

        then

         A77: (o,c1) // (b1,a1) by A6, A76, ANALMETR: 60;

        (o,c) // (o,c1) by A12, ANALMETR:def 10;

        then

         A78: (o,c1) _|_ (o,c2) by A6, A18, ANALMETR: 62;

        (c,b) _|_ (c2,b2) by A40, ANALMETR: 61;

        then (b,a) _|_ (b2,a2) by A1, A18, A32, A48, A71, A50, A38, A36, CONAFFM:def 2;

        then (b2,a2) _|_ (a,b) by ANALMETR: 61;

        then (b2,a2) _|_ (a1,b1) by A13, A35, ANALMETR: 62;

        then

         A79: (b1,a1) _|_ (b2,a2) by ANALMETR: 61;

        (o,a) // (o,a1) by A10, ANALMETR:def 10;

        then (o,a1) _|_ (o,a2) by A2, A48, ANALMETR: 62;

        then (o,a2) // (o,a3) by A3, A66, ANALMETR: 63;

        then LIN (o,a2,a3) by ANALMETR:def 10;

        then

         A80: LIN (o9,a29,a39) by ANALMETR: 40;

         LIN (c2,e2,a3) by A65, ANALMETR: 40;

        then (c2,e2) // (c2,a3) by ANALMETR:def 10;

        then

         A81: (a1,c1) _|_ (c2,a3) by A60, A61, ANALMETR: 62;

        then (c1,a1) _|_ (c2,a3) by ANALMETR: 61;

        then (b1,a1) _|_ (b2,a3) by A1, A66, A78, A33, A67, A77, A68, A72, CONAFFM:def 2;

        then (b2,a3) // (b2,a2) by A22, A79, ANALMETR: 63;

        then (b29,a39) // (b29,a29) by ANALMETR: 36;

        then (b29,a29) // (b29,a39) by AFF_1: 4;

        then a29 = a39 by A51, A80, AFF_1: 14;

        then (c,a) // (a1,c1) by A50, A81, A49, ANALMETR: 63;

        then (c9,a9) // (a19,c19) by ANALMETR: 36;

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

        hence thesis by ANALMETR: 36;

      end;

      now

        assume

         A82: LIN (a,b,c);

        then

         A83: LIN (a9,b9,c9) by ANALMETR: 40;

        

         A84: a <> b

        proof

          assume a = b;

          then LIN (b9,b19,a9) by AFF_1: 7;

          hence contradiction by A8, ANALMETR: 40;

        end;

         A85:

        now

          assume (a1,c1) // (a,b);

          then (a19,c19) // (a9,b9) by ANALMETR: 36;

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

          then

           A86: (a,b) // (a1,c1) by ANALMETR: 36;

          (a,b) // (a,c) by A82, ANALMETR:def 10;

          hence thesis by A84, A86, ANALMETR: 60;

        end;

        

         A87: b <> c

        proof

          assume b = c;

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

          hence contradiction by A9, ANALMETR: 40;

        end;

         A88:

        now

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

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

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

          then

           A89: (b,c) // (a,c) by ANALMETR: 36;

          assume a1 = b1;

          hence thesis by A15, A87, A89, ANALMETR: 60;

        end;

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

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

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

        then (a,b) // (b,c) by ANALMETR: 36;

        then (b,c) // (a1,b1) by A13, A84, ANALMETR: 60;

        then (b1,c1) // (a1,b1) by A15, A87, ANALMETR: 60;

        then (b19,c19) // (a19,b19) by ANALMETR: 36;

        then (b19,a19) // (b19,c19) by AFF_1: 4;

        then LIN (b19,a19,c19) by AFF_1:def 1;

        then LIN (a19,b19,c19) by AFF_1: 6;

        then LIN (a1,b1,c1) by ANALMETR: 40;

        then

         A90: (a1,b1) // (a1,c1) by ANALMETR:def 10;

        (a9,b9) // (a19,b19) by A13, ANALMETR: 36;

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

        then (a1,b1) // (a,b) by ANALMETR: 36;

        hence thesis by A90, A85, A88, ANALMETR: 60;

      end;

      hence thesis by A28;

    end;

    theorem :: CONMETR:12

    X is satisfying_OSCH & X is satisfying_TDES implies X is satisfying_SCH

    proof

      assume that

       A1: X is satisfying_OSCH and

       A2: X is satisfying_TDES;

      let a1, a2, a3, a4, b1, b2, b3, b4, M, N;

      assume that

       A3: M is being_line and

       A4: N is being_line and

       A5: a1 in M and

       A6: a3 in M and

       A7: b1 in M and

       A8: b3 in M and

       A9: a2 in N and

       A10: a4 in N and

       A11: b2 in N and

       A12: b4 in N and

       A13: not a4 in M and

       A14: not a2 in M and

       A15: not b2 in M and

       A16: not b4 in M and

       A17: not a1 in N and

       A18: not a3 in N and

       A19: not b1 in N and

       A20: not b3 in N and

       A21: (a3,a2) // (b3,b2) and

       A22: (a2,a1) // (b2,b1) and

       A23: (a1,a4) // (b1,b4);

      reconsider a19 = a1, a29 = a2, a39 = a3, a49 = a4, b19 = b1, b29 = b2, b39 = b3, b49 = b4 as Element of the AffinStruct of X;

      reconsider M9 = M, N9 = N as Subset of the AffinStruct of X;

      

       A24: M9 is being_line by A3, ANALMETR: 43;

      

       A25: N9 is being_line by A4, ANALMETR: 43;

      

       A26: a1 <> b1 implies a2 <> b2 & a3 <> b3 & a4 <> b4

      proof

        assume

         A27: a1 <> b1;

         A28:

        now

          assume a4 = b4;

          then (a4,a1) // (a4,b1) by A23, ANALMETR: 59;

          then LIN (a4,a1,b1) by ANALMETR:def 10;

          then LIN (a49,a19,b19) by ANALMETR: 40;

          then LIN (a19,b19,a49) by AFF_1: 6;

          hence contradiction by A5, A7, A13, A24, A27, AFF_1: 25;

        end;

         A29:

        now

          assume a2 = b2;

          then LIN (a2,a1,b1) by A22, ANALMETR:def 10;

          then LIN (a29,a19,b19) by ANALMETR: 40;

          then LIN (a19,b19,a29) by AFF_1: 6;

          hence contradiction by A5, A7, A14, A24, A27, AFF_1: 25;

        end;

         A30:

        now

          assume a3 = b3;

          then LIN (a3,a2,b2) by A21, ANALMETR:def 10;

          then LIN (a39,a29,b29) by ANALMETR: 40;

          then LIN (a29,b29,a39) by AFF_1: 6;

          hence contradiction by A9, A11, A18, A25, A29, AFF_1: 25;

        end;

        assume a2 = b2 or a3 = b3 or a4 = b4;

        hence contradiction by A29, A28, A30;

      end;

       A31:

      now

        assume

         A32: a1 <> b1;

         A33:

        now

          

           A34: not LIN (a29,b19,b29)

          proof

            assume LIN (a29,b19,b29);

            then LIN (a29,b29,b19) by AFF_1: 6;

            hence contradiction by A9, A11, A19, A25, A26, A32, AFF_1: 25;

          end;

          assume

           A35: a2 = a4;

          then (a2,a1) // (b1,b4) by A23, ANALMETR: 59;

          then (b2,b1) // (b1,b4) by A5, A14, A22, ANALMETR: 60;

          then (b1,b2) // (b1,b4) by ANALMETR: 59;

          then

           A36: (b19,b29) // (b19,b49) by ANALMETR: 36;

          (a29,b29) // (a29,b49) by A9, A11, A12, A25, AFF_1: 39, AFF_1: 41;

          then LIN (a29,b29,b49) by AFF_1:def 1;

          hence thesis by A21, A35, A34, A36, AFF_1: 14;

        end;

         A37:

        now

          assume that

           A38: a2 <> a4 and

           A39: a1 <> a3;

           A40:

          now

            consider e1 be Element of X such that

             A41: (b1,b2) // (b1,e1) and

             A42: b1 <> e1 by ANALMETR: 39;

            consider x be Element of X such that

             A43: LIN (a1,a2,x) and

             A44: a1 <> x and

             A45: a2 <> x by Th2;

            reconsider x9 = x as Element of the AffinStruct of X;

            consider e2 be Element of X such that

             A46: (a1,b1) // (x,e2) and

             A47: x <> e2 by ANALMETR: 39;

            reconsider e19 = e1, e29 = e2 as Element of the AffinStruct of X;

             not (b19,e19) // (x9,e29)

            proof

              assume (b19,e19) // (x9,e29);

              then (b1,e1) // (x,e2) by ANALMETR: 36;

              then (b1,b2) // (x,e2) by A41, A42, ANALMETR: 60;

              then (b1,b2) // (a1,b1) by A46, A47, ANALMETR: 60;

              then (b1,a1) // (b1,b2) by ANALMETR: 59;

              then LIN (b1,a1,b2) by ANALMETR:def 10;

              then LIN (b19,a19,b29) by ANALMETR: 40;

              hence contradiction by A5, A7, A15, A24, A32, AFF_1: 25;

            end;

            then

            consider y9 be Element of the AffinStruct of X such that

             A48: LIN (b19,e19,y9) and

             A49: LIN (x9,e29,y9) by AFF_1: 60;

            reconsider y = y9 as Element of X;

            

             A50: (a1,a2) // (a1,x) by A43, ANALMETR:def 10;

            

             A51: not LIN (a2,b2,x)

            proof

              

               A52: a2 <> b2

              proof

                assume a2 = b2;

                then LIN (a2,a1,b1) by A22, ANALMETR:def 10;

                then LIN (a29,a19,b19) by ANALMETR: 40;

                then LIN (a19,b19,a29) by AFF_1: 6;

                hence contradiction by A5, A7, A14, A24, A32, AFF_1: 25;

              end;

               LIN (a19,a29,x9) by A43, ANALMETR: 40;

              then

               A53: LIN (a29,x9,a19) by AFF_1: 6;

              assume LIN (a2,b2,x);

              then LIN (a29,b29,x9) by ANALMETR: 40;

              then x9 in N9 by A9, A11, A25, A52, AFF_1: 25;

              hence contradiction by A9, A17, A25, A45, A53, AFF_1: 25;

            end;

            

             A54: not LIN (a1,b1,a4)

            proof

              assume LIN (a1,b1,a4);

              then LIN (a19,b19,a49) by ANALMETR: 40;

              hence contradiction by A5, A7, A13, A24, A32, AFF_1: 25;

            end;

            

             A55: not LIN (a1,b1,x)

            proof

              assume LIN (a1,b1,x);

              then LIN (a19,b19,x9) by ANALMETR: 40;

              then

               A56: x9 in M9 by A5, A7, A24, A32, AFF_1: 25;

               LIN (a19,a29,x9) by A43, ANALMETR: 40;

              then LIN (a19,x9,a29) by AFF_1: 6;

              hence contradiction by A5, A14, A24, A44, A56, AFF_1: 25;

            end;

            assume

             A57: M // N;

            then M9 // N9 by ANALMETR: 46;

            then (a39,b39) // (a29,b29) by A6, A8, A9, A11, AFF_1: 39;

            then (a3,b3) // (a2,b2) by ANALMETR: 36;

            then

             A58: (a2,b2) // (a3,b3) by ANALMETR: 59;

             LIN (x,e2,y) by A49, ANALMETR: 40;

            then (x,e2) // (x,y) by ANALMETR:def 10;

            then

             A59: (a1,b1) // (x,y) by A46, A47, ANALMETR: 60;

            

             A60: b1 <> y

            proof

              assume b1 = y;

              then (b1,a1) // (b1,x) by A59, ANALMETR: 59;

              then LIN (b1,a1,x) by ANALMETR:def 10;

              then LIN (b19,a19,x9) by ANALMETR: 40;

              then

               A61: x9 in M9 by A5, A7, A24, A32, AFF_1: 25;

               LIN (a19,a29,x9) by A43, ANALMETR: 40;

              then LIN (a19,x9,a29) by AFF_1: 6;

              hence contradiction by A5, A14, A24, A44, A61, AFF_1: 25;

            end;

             LIN (b1,e1,y) by A48, ANALMETR: 40;

            then (b1,e1) // (b1,y) by ANALMETR:def 10;

            then

             A62: (b1,b2) // (b1,y) by A41, A42, ANALMETR: 60;

            then LIN (b1,b2,y) by ANALMETR:def 10;

            then LIN (b19,b29,y9) by ANALMETR: 40;

            then LIN (y9,b19,b29) by AFF_1: 6;

            then LIN (y,b1,b2) by ANALMETR: 40;

            then (y,b1) // (y,b2) by ANALMETR:def 10;

            then

             A63: (b1,y) // (b2,y) by ANALMETR: 59;

            (a1,a2) // (b1,b2) by A22, ANALMETR: 59;

            then (a1,a2) // (b1,y) by A7, A15, A62, ANALMETR: 60;

            then

             A64: (a1,x) // (b1,y) by A5, A14, A50, ANALMETR: 60;

            

             A65: not LIN (x,y,a3)

            proof

              

               A66: x <> y

              proof

                assume x = y;

                then (x,a1) // (x,b1) by A64, ANALMETR: 59;

                then LIN (x,a1,b1) by ANALMETR:def 10;

                then LIN (x9,a19,b19) by ANALMETR: 40;

                then LIN (a19,b19,x9) by AFF_1: 6;

                then

                 A67: x9 in M9 by A5, A7, A24, A32, AFF_1: 25;

                 LIN (a19,a29,x9) by A43, ANALMETR: 40;

                then LIN (x9,a19,a29) by AFF_1: 6;

                hence contradiction by A5, A14, A24, A44, A67, AFF_1: 25;

              end;

              (a19,a39) // (a19,b19) by A5, A6, A7, A24, AFF_1: 39, AFF_1: 41;

              then (a1,a3) // (a1,b1) by ANALMETR: 36;

              then

               A68: (x,y) // (a1,a3) by A32, A59, ANALMETR: 60;

              assume LIN (x,y,a3);

              then (x,y) // (x,a3) by ANALMETR:def 10;

              then (x,a3) // (a1,a3) by A66, A68, ANALMETR: 60;

              then (a3,a1) // (a3,x) by ANALMETR: 59;

              then LIN (a3,a1,x) by ANALMETR:def 10;

              then LIN (a39,a19,x9) by ANALMETR: 40;

              then

               A69: x9 in M9 by A5, A6, A24, A39, AFF_1: 25;

               LIN (a19,a29,x9) by A43, ANALMETR: 40;

              then LIN (a19,x9,a29) by AFF_1: 6;

              hence contradiction by A5, A14, A24, A44, A69, AFF_1: 25;

            end;

            

             A70: not LIN (x,y,a4)

            proof

              

               A71: x <> y

              proof

                assume x = y;

                then (x,a1) // (x,b1) by A64, ANALMETR: 59;

                then LIN (x,a1,b1) by ANALMETR:def 10;

                then LIN (x9,a19,b19) by ANALMETR: 40;

                then LIN (a19,b19,x9) by AFF_1: 6;

                then

                 A72: x9 in M9 by A5, A7, A24, A32, AFF_1: 25;

                 LIN (a19,a29,x9) by A43, ANALMETR: 40;

                then LIN (x9,a19,a29) by AFF_1: 6;

                hence contradiction by A5, A14, A24, A44, A72, AFF_1: 25;

              end;

              M9 // N9 by A57, ANALMETR: 46;

              then (a19,b19) // (a29,a49) by A5, A7, A9, A10, AFF_1: 39;

              then (a1,b1) // (a2,a4) by ANALMETR: 36;

              then

               A73: (a2,a4) // (x,y) by A32, A59, ANALMETR: 60;

              assume LIN (x,y,a4);

              then (x,y) // (x,a4) by ANALMETR:def 10;

              then (a2,a4) // (x,a4) by A71, A73, ANALMETR: 60;

              then (a4,a2) // (a4,x) by ANALMETR: 59;

              then LIN (a4,a2,x) by ANALMETR:def 10;

              then LIN (a49,a29,x9) by ANALMETR: 40;

              then

               A74: x9 in N9 by A9, A10, A25, A38, AFF_1: 25;

               LIN (a19,a29,x9) by A43, ANALMETR: 40;

              then LIN (a29,x9,a19) by AFF_1: 6;

              hence contradiction by A9, A17, A25, A45, A74, AFF_1: 25;

            end;

            

             A75: not LIN (a2,b2,a3)

            proof

              

               A76: a2 <> b2

              proof

                assume a2 = b2;

                then LIN (a2,a1,b1) by A22, ANALMETR:def 10;

                then LIN (a29,a19,b19) by ANALMETR: 40;

                then LIN (a19,b19,a29) by AFF_1: 6;

                hence contradiction by A5, A7, A14, A24, A32, AFF_1: 25;

              end;

              assume LIN (a2,b2,a3);

              then LIN (a29,b29,a39) by ANALMETR: 40;

              hence contradiction by A9, A11, A18, A25, A76, AFF_1: 25;

            end;

            

             A77: X is satisfying_TDES implies X is satisfying_des

            proof

              assume X is satisfying_TDES;

              then the AffinStruct of X is Moufangian by Th7;

              then the AffinStruct of X is translational by AFF_2: 14;

              hence thesis by Th8;

            end;

             LIN (a19,a29,x9) by A43, ANALMETR: 40;

            then LIN (x9,a19,a29) by AFF_1: 6;

            then LIN (x,a1,a2) by ANALMETR: 40;

            then (x,a1) // (x,a2) by ANALMETR:def 10;

            then (a1,x) // (a2,x) by ANALMETR: 59;

            then (a2,x) // (b1,y) by A44, A64, ANALMETR: 60;

            then

             A78: (a2,x) // (b2,y) by A60, A63, ANALMETR: 60;

            (a19,b19) // (a39,b39) by A5, A6, A7, A8, A24, AFF_1: 39, AFF_1: 41;

            then (a1,b1) // (a3,b3) by ANALMETR: 36;

            then

             A79: (x,y) // (a3,b3) by A32, A59, ANALMETR: 60;

            M9 // N9 by A57, ANALMETR: 46;

            then (a19,b19) // (a49,b49) by A5, A7, A10, A12, AFF_1: 39;

            then (a1,b1) // (a4,b4) by ANALMETR: 36;

            then

             A80: (x,y) // (a4,b4) by A32, A59, ANALMETR: 60;

            M9 // N9 by A57, ANALMETR: 46;

            then (a19,b19) // (a29,b29) by A5, A7, A9, A11, AFF_1: 39;

            then (a1,b1) // (a2,b2) by ANALMETR: 36;

            then

             A81: (a2,b2) // (x,y) by A32, A59, ANALMETR: 60;

            (a2,a3) // (b2,b3) by A21, ANALMETR: 59;

            then

             A82: (x,a3) // (y,b3) by A2, A77, A51, A75, A81, A58, A78;

            M9 // N9 by A57, ANALMETR: 46;

            then (a19,b19) // (a49,b49) by A5, A7, A10, A12, AFF_1: 39;

            then (a1,b1) // (a4,b4) by ANALMETR: 36;

            then (x,a4) // (y,b4) by A2, A23, A59, A77, A55, A54, A64;

            hence thesis by A2, A77, A82, A65, A70, A79, A80;

          end;

          now

            assume not M // N;

            then not M9 // N9 by ANALMETR: 46;

            then

            consider o9 be Element of the AffinStruct of X such that

             A83: o9 in M9 and

             A84: o9 in N9 by A24, A25, AFF_1: 58;

            reconsider o = o9 as Element of X;

            consider K such that

             A85: o in K and

             A86: N _|_ K by A4, Th3;

            reconsider K9 = K as Subset of the AffinStruct of X;

            

             A87: K is being_line by A86, ANALMETR: 44;

            then

             A88: K9 is being_line by ANALMETR: 43;

            now

              

               A89: not a2 in K & not a4 in K & not b2 in K & not b4 in K

              proof

                 A90:

                now

                  let x be Element of X;

                  assume that

                   A91: x in N and

                   A92: o <> x;

                  assume x in K;

                  then (o,x) _|_ (o,x) by A84, A85, A86, A91, ANALMETR: 56;

                  hence contradiction by A92, ANALMETR: 39;

                end;

                assume not thesis;

                hence contradiction by A9, A10, A11, A12, A13, A14, A15, A16, A83, A90;

              end;

              

               A93: LIN (o,a2,b2) by A4, A9, A11, A84, Th4;

               A94:

              now

                assume LIN (a1,b1,a4);

                then LIN (a19,b19,a49) by ANALMETR: 40;

                hence contradiction by A5, A7, A13, A24, A32, AFF_1: 25;

              end;

              

               A95: LIN (o,a3,b3) by A3, A6, A8, A83, Th4;

               A96:

              now

                assume LIN (a3,b3,a2);

                then LIN (a39,b39,a29) by ANALMETR: 40;

                hence contradiction by A6, A8, A14, A24, A26, A32, AFF_1: 25;

              end;

              

               A97: LIN (o,a1,b1) by A3, A5, A7, A83, Th4;

               A98:

              now

                let x9 be Element of the AffinStruct of X;

                consider D9 be Subset of the AffinStruct of X such that

                 A99: x9 in D9 and

                 A100: N9 // D9 by A25, AFF_1: 49;

                reconsider D = D9 as Subset of the carrier of X;

                N // D by A100, ANALMETR: 46;

                then K _|_ D by A86, ANALMETR: 52;

                then

                consider y be Element of X such that

                 A101: y in K and

                 A102: y in D by ANALMETR: 66;

                reconsider y9 = y as Element of the AffinStruct of X;

                take y9;

                thus y9 in K9 & (x9,y9) // N9 by A99, A100, A101, A102, AFF_1: 40;

              end;

              then

              consider d19 be Element of the AffinStruct of X such that

               A103: d19 in K9 and

               A104: (a19,d19) // N9;

              consider e19 be Element of the AffinStruct of X such that

               A105: e19 in K9 and

               A106: (b19,e19) // N9 by A98;

              consider d39 be Element of the AffinStruct of X such that

               A107: d39 in K9 and

               A108: (a39,d39) // N9 by A98;

              consider e39 be Element of the AffinStruct of X such that

               A109: e39 in K9 and

               A110: (b39,e39) // N9 by A98;

              reconsider d1 = d19, d3 = d39, e1 = e19, e3 = e39 as Element of X;

              

               A111: LIN (o,d1,e1) by A85, A87, A103, A105, Th4;

              

               A112: o <> e1 & o <> e3 & o <> d1 & o <> d3

              proof

                 A113:

                now

                  let x,y be Element of X, x9,y9 be Element of the AffinStruct of X;

                  assume that

                   A114: (x9,y9) // N9 and

                   A115: x = x9 and

                   A116: y = y9 and x in M and y in K and

                   A117: not x in N;

                  assume o = y;

                  then (o9,x9) // N9 by A114, A116, AFF_1: 34;

                  hence contradiction by A25, A84, A115, A117, AFF_1: 23;

                end;

                assume not thesis;

                hence contradiction by A5, A6, A7, A8, A17, A18, A19, A20, A103, A104, A107, A108, A109, A110, A105, A106, A113;

              end;

              (a1,d1) // (o,a2) by A9, A84, A104, Th6;

              then

               A118: (d1,a1) // (o,a2) by ANALMETR: 59;

              

               A119: not e1 in N by A19, A106, AFF_1: 35;

              

               A120: not d3 in N by A18, A108, AFF_1: 35;

              (a19,d19) // (b19,e19) by A25, A104, A106, AFF_1: 31;

              then (a1,d1) // (b1,e1) by ANALMETR: 36;

              then

               A121: (d1,a1) // (e1,b1) by ANALMETR: 59;

              assume

               A122: K <> M;

               A123:

              now

                assume LIN (a3,b3,d3);

                then LIN (a39,b39,d39) by ANALMETR: 40;

                then d3 in M by A6, A8, A24, A26, A32, AFF_1: 25;

                hence contradiction by A3, A83, A85, A87, A122, A107, A112, Th5;

              end;

               A124:

              now

                assume LIN (a1,b1,d1);

                then LIN (a19,b19,d19) by ANALMETR: 40;

                then d1 in M by A5, A7, A24, A32, AFF_1: 25;

                hence contradiction by A3, A83, A85, A87, A122, A103, A112, Th5;

              end;

              (a39,d39) // (b39,e39) by A25, A108, A110, AFF_1: 31;

              then

               A125: (a3,d3) // (b3,e3) by ANALMETR: 36;

              then

               A126: (d3,a3) // (e3,b3) by ANALMETR: 59;

              

               A127: not LIN (d3,e3,a3) & not LIN (d3,e3,a4)

              proof

                

                 A128: d3 <> e3

                proof

                  assume not thesis;

                  then LIN (e3,a3,b3) by A126, ANALMETR:def 10;

                  then LIN (e39,a39,b39) by ANALMETR: 40;

                  then LIN (a39,b39,e39) by AFF_1: 6;

                  then e39 in M9 by A6, A8, A24, A26, A32, AFF_1: 25;

                  hence contradiction by A24, A83, A85, A88, A122, A109, A112, AFF_1: 18;

                end;

                assume not thesis;

                then LIN (d39,e39,a39) or LIN (d39,e39,a49) by ANALMETR: 40;

                then a39 in K9 or a49 in K9 by A88, A107, A109, A128, AFF_1: 25;

                hence contradiction by A6, A10, A13, A18, A24, A25, A83, A84, A85, A86, A88, A122, AFF_1: 18;

              end;

               A129:

              now

                assume LIN (a1,b1,a2);

                then LIN (a19,b19,a29) by ANALMETR: 40;

                hence contradiction by A5, A7, A14, A24, A32, AFF_1: 25;

              end;

              

               A130: LIN (o,a4,b4) by A4, A10, A12, A84, Th4;

              (a1,a2) // (b1,b2) by A22, ANALMETR: 59;

              then (d1,a2) // (e1,b2) by A2, A14, A15, A17, A19, A83, A84, A112, A93, A97, A111, A124, A129, A121, A118;

              then

               A131: (a2,d1) // (b2,e1) by ANALMETR: 59;

              

               A132: not e3 in N by A20, A110, AFF_1: 35;

              

               A133: LIN (o,d3,e3) by A85, A87, A107, A109, Th4;

              (a1,d1) // (o,a4) by A10, A84, A104, Th6;

              then (d1,a1) // (o,a4) by ANALMETR: 59;

              then

               A134: (d1,a4) // (e1,b4) by A2, A13, A16, A17, A19, A23, A83, A84, A112, A97, A130, A111, A124, A94, A121;

              

               A135: (a3,d3) // (o,a4) by A10, A84, A108, Th6;

              

               A136: not d1 in N by A17, A104, AFF_1: 35;

              (a3,d3) // (o,a2) by A9, A84, A108, Th6;

              then (d3,a3) // (o,a2) by ANALMETR: 59;

              then (d3,a2) // (e3,b2) by A2, A14, A15, A18, A20, A21, A83, A84, A112, A93, A95, A133, A123, A96, A126;

              then (d3,a4) // (e3,b4) by A1, A9, A10, A11, A12, A86, A103, A107, A109, A105, A131, A134, A136, A120, A119, A132, A89;

              hence thesis by A2, A13, A16, A18, A20, A83, A84, A112, A130, A95, A133, A125, A127, A135;

            end;

            hence thesis by A1, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23, A86;

          end;

          hence thesis by A40;

        end;

        now

          

           A137: not LIN (a19,b29,b19)

          proof

            assume LIN (a19,b29,b19);

            then LIN (a19,b19,b29) by AFF_1: 6;

            hence contradiction by A5, A7, A15, A24, A32, AFF_1: 25;

          end;

          (a19,b19) // (a19,b39) by A5, A7, A8, A24, AFF_1: 39, AFF_1: 41;

          then

           A138: LIN (a19,b19,b39) by AFF_1:def 1;

          assume

           A139: a1 = a3;

          then (a2,a1) // (b2,b3) by A21, ANALMETR: 59;

          then (b2,b1) // (b2,b3) by A5, A14, A22, ANALMETR: 60;

          then (b29,b19) // (b29,b39) by ANALMETR: 36;

          hence thesis by A23, A139, A137, A138, AFF_1: 14;

        end;

        hence thesis by A33, A37;

      end;

      

       A140: a1 = b1 implies a2 = b2 & a3 = b3 & a4 = b4

      proof

        assume

         A141: a1 = b1;

         A142:

        now

           LIN (a1,a4,b4) by A23, A141, ANALMETR:def 10;

          then LIN (a19,a49,b49) by ANALMETR: 40;

          then

           A143: LIN (a49,b49,a19) by AFF_1: 6;

          assume a4 <> b4;

          hence contradiction by A10, A12, A17, A25, A143, AFF_1: 25;

        end;

         A144:

        now

          (a1,a2) // (a1,b2) by A22, A141, ANALMETR: 59;

          then LIN (a1,a2,b2) by ANALMETR:def 10;

          then LIN (a19,a29,b29) by ANALMETR: 40;

          then

           A145: LIN (a29,b29,a19) by AFF_1: 6;

          assume a2 <> b2;

          hence contradiction by A9, A11, A17, A25, A145, AFF_1: 25;

        end;

         A146:

        now

          (a2,a3) // (a2,b3) by A21, A144, ANALMETR: 59;

          then LIN (a2,a3,b3) by ANALMETR:def 10;

          then LIN (a29,a39,b39) by ANALMETR: 40;

          then

           A147: LIN (a39,b39,a29) by AFF_1: 6;

          assume a3 <> b3;

          hence contradiction by A6, A8, A14, A24, A147, AFF_1: 25;

        end;

        assume a2 <> b2 or a3 <> b3 or a4 <> b4;

        hence contradiction by A144, A142, A146;

      end;

      now

        assume a1 = b1;

        then (a39,a49) // (b39,b49) by A140, AFF_1: 2;

        hence thesis by ANALMETR: 36;

      end;

      hence thesis by A31;

    end;

    theorem :: CONMETR:13

    X is satisfying_OPAP & X is satisfying_DES implies X is satisfying_PAP

    proof

      assume that

       A1: X is satisfying_OPAP and

       A2: X is satisfying_DES;

      let o, a1, a2, a3, b1, b2, b3, M, N;

      assume that

       A3: M is being_line and

       A4: N is being_line and

       A5: o in M and

       A6: a1 in M and

       A7: a2 in M and

       A8: a3 in M and

       A9: o in N and

       A10: b1 in N and

       A11: b2 in N and

       A12: b3 in N and

       A13: not b2 in M and

       A14: not a3 in N and

       A15: o <> a1 and

       A16: o <> a2 and o <> a3 and

       A17: o <> b1 and o <> b2 and

       A18: o <> b3 and

       A19: (a3,b2) // (a2,b1) and

       A20: (a3,b3) // (a1,b1);

      reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, b19 = b1, b29 = b2, b39 = b3 as Element of the AffinStruct of X;

      reconsider M9 = M, N9 = N as Subset of the AffinStruct of X;

      

       A21: M9 is being_line by A3, ANALMETR: 43;

      

       A22: N9 is being_line by A4, ANALMETR: 43;

      now

        assume

         A23: not M _|_ N;

         A24:

        now

          assume that

           A25: a1 <> a2 and

           A26: a2 <> a3 and

           A27: a1 <> a3;

          

           A28: b1 <> b2 & b2 <> b3 & b1 <> b3

          proof

             A29:

            now

              

               A30: not LIN (o9,b19,a19)

              proof

                (o9,a19) // (o9,a39) by A5, A6, A8, A21, AFF_1: 39, AFF_1: 41;

                then

                 A31: LIN (o9,a19,a39) by AFF_1:def 1;

                assume LIN (o9,b19,a19);

                then a19 in N9 by A9, A10, A17, A22, AFF_1: 25;

                hence contradiction by A9, A14, A15, A22, A31, AFF_1: 25;

              end;

              assume b1 = b3;

              then (b1,a1) // (b1,a3) by A20, ANALMETR: 59;

              then

               A32: (b19,a19) // (b19,a39) by ANALMETR: 36;

              (o9,a19) // (o9,a39) by A5, A6, A8, A21, AFF_1: 39, AFF_1: 41;

              then LIN (o9,a19,a39) by AFF_1:def 1;

              hence contradiction by A27, A30, A32, AFF_1: 14;

            end;

             A33:

            now

              

               A34: not LIN (o9,b19,a19)

              proof

                (o9,a19) // (o9,a39) by A5, A6, A8, A21, AFF_1: 39, AFF_1: 41;

                then

                 A35: LIN (o9,a19,a39) by AFF_1:def 1;

                assume LIN (o9,b19,a19);

                then a19 in N9 by A9, A10, A17, A22, AFF_1: 25;

                hence contradiction by A9, A14, A15, A22, A35, AFF_1: 25;

              end;

              assume b2 = b3;

              then (a1,b1) // (a2,b1) by A8, A13, A19, A20, ANALMETR: 60;

              then (b1,a1) // (b1,a2) by ANALMETR: 59;

              then

               A36: (b19,a19) // (b19,a29) by ANALMETR: 36;

              (o9,a19) // (o9,a29) by A5, A6, A7, A21, AFF_1: 39, AFF_1: 41;

              then LIN (o9,a19,a29) by AFF_1:def 1;

              hence contradiction by A25, A34, A36, AFF_1: 14;

            end;

             A37:

            now

              

               A38: not LIN (o9,b29,a29)

              proof

                assume LIN (o9,b29,a29);

                then LIN (o9,a29,b29) by AFF_1: 6;

                hence contradiction by A5, A7, A13, A16, A21, AFF_1: 25;

              end;

              assume b1 = b2;

              then (b2,a2) // (b2,a3) by A19, ANALMETR: 59;

              then

               A39: (b29,a29) // (b29,a39) by ANALMETR: 36;

              (o9,a29) // (o9,a39) by A5, A7, A8, A21, AFF_1: 39, AFF_1: 41;

              then LIN (o9,a29,a39) by AFF_1:def 1;

              hence contradiction by A26, A38, A39, AFF_1: 14;

            end;

            assume b1 = b2 or b2 = b3 or b1 = b3;

            hence contradiction by A37, A33, A29;

          end;

           A40:

          now

            

             A41: not LIN (b3,b1,a3)

            proof

              assume LIN (b3,b1,a3);

              then LIN (b39,b19,a39) by ANALMETR: 40;

              hence contradiction by A10, A12, A14, A22, A28, AFF_1: 25;

            end;

            (o9,b29) // (o9,b39) by A9, A11, A12, A22, AFF_1: 39, AFF_1: 41;

            then LIN (o9,b29,b39) by AFF_1:def 1;

            then

             A42: LIN (o,b2,b3) by ANALMETR: 40;

            

             A43: not LIN (b2,b1,a3)

            proof

              assume LIN (b2,b1,a3);

              then LIN (b29,b19,a39) by ANALMETR: 40;

              hence contradiction by A10, A11, A14, A22, A28, AFF_1: 25;

            end;

            (o9,a39) // (o9,a19) by A5, A6, A8, A21, AFF_1: 39, AFF_1: 41;

            then LIN (o9,a39,a19) by AFF_1:def 1;

            then

             A44: LIN (o,a3,a1) by ANALMETR: 40;

            consider x be Element of X such that

             A45: (o,b2) _|_ (o,x) and

             A46: o <> x by ANALMETR: 39;

            

             A47: (o,x) _|_ N by A4, A5, A9, A11, A13, A45, ANALMETR: 55;

            consider e19 be Element of the AffinStruct of X such that

             A48: (a39,b39) // (b29,e19) and

             A49: b29 <> e19 by DIRAF: 40;

            reconsider x9 = x as Element of the AffinStruct of X;

             LIN (o9,x9,x9) by AFF_1: 7;

            then

            consider A9 be Subset of the AffinStruct of X such that

             A50: A9 is being_line and

             A51: o9 in A9 and

             A52: x9 in A9 and x9 in A9 by AFF_1: 21;

            reconsider A = A9 as Subset of X;

            

             A53: for e1 holds e1 in A implies LIN (o,x,e1)

            proof

              let e1 such that

               A54: e1 in A;

              reconsider e19 = e1 as Element of the AffinStruct of X;

              (o9,x9) // (o9,e19) by A50, A51, A52, A54, AFF_1: 39, AFF_1: 41;

              then LIN (o9,x9,e19) by AFF_1:def 1;

              hence thesis by ANALMETR: 40;

            end;

            for e1 holds LIN (o,x,e1) implies e1 in A

            proof

              let e1 such that

               A55: LIN (o,x,e1);

              reconsider e19 = e1 as Element of the AffinStruct of X;

               LIN (o9,x9,e19) by A55, ANALMETR: 40;

              hence thesis by A46, A50, A51, A52, AFF_1: 25;

            end;

            then A = ( Line (o,x)) by A53, ANALMETR:def 11;

            then

             A56: A _|_ N by A46, A47, ANALMETR:def 14;

            

             A57: not b2 in A

            proof

              

               A58: (o9,b29) // (o9,b29) by AFF_1: 2;

              assume b2 in A;

              then A9 // N9 by A5, A9, A11, A13, A22, A50, A51, A58, AFF_1: 38;

              then A // N by ANALMETR: 46;

              hence contradiction by A56, ANALMETR: 52;

            end;

            assume

             A59: not (a3,b3) _|_ (o,b2);

             not (b29,e19) // A9

            proof

              assume

               A60: (b29,e19) // A9;

              consider d19,d29 be Element of the AffinStruct of X such that

               A61: d19 <> d29 and

               A62: A9 = ( Line (d19,d29)) by A50, AFF_1:def 3;

              

               A63: d29 in A9 by A62, AFF_1: 15;

              reconsider d1 = d19, d2 = d29 as Element of X;

              (d19,d29) // (d19,d29) by AFF_1: 2;

              then (d19,d29) // A9 by A61, A62, AFF_1:def 4;

              then (b29,e19) // (d19,d29) by A50, A60, AFF_1: 31;

              then (a39,b39) // (d19,d29) by A48, A49, AFF_1: 5;

              then

               A64: (a3,b3) // (d1,d2) by ANALMETR: 36;

              d19 in A9 by A62, AFF_1: 15;

              then (d1,d2) _|_ (o,b2) by A9, A11, A56, A63, ANALMETR: 56;

              hence contradiction by A59, A61, A64, ANALMETR: 62;

            end;

            then

            consider c39 be Element of the AffinStruct of X such that

             A65: c39 in A9 and

             A66: LIN (b29,e19,c39) by A50, AFF_1: 59;

            (b29,e19) // (b29,c39) by A66, AFF_1:def 1;

            then

             A67: (a39,b39) // (b29,c39) by A48, A49, AFF_1: 5;

            consider e19 be Element of the AffinStruct of X such that

             A68: (c39,a39) // (a19,e19) and

             A69: a19 <> e19 by DIRAF: 40;

             not (a19,e19) // A9

            proof

              

               A70: c39 <> o9

              proof

                assume c39 = o9;

                then

                 A71: (a3,b3) // (b2,o) by A67, ANALMETR: 36;

                (b29,o9) // (b29,b39) by A9, A11, A12, A22, AFF_1: 39, AFF_1: 41;

                then (b2,o) // (b2,b3) by ANALMETR: 36;

                then (a3,b3) // (b2,b3) by A5, A13, A71, ANALMETR: 60;

                then (b3,b2) // (b3,a3) by ANALMETR: 59;

                then LIN (b3,b2,a3) by ANALMETR:def 10;

                then LIN (b39,b29,a39) by ANALMETR: 40;

                hence contradiction by A11, A12, A14, A22, A28, AFF_1: 25;

              end;

              assume

               A72: (a19,e19) // A9;

              

               A73: (o9,a39) // (o9,a39) by AFF_1: 2;

              (o9,c39) // A9 by A50, A51, A65, AFF_1: 40, AFF_1: 41;

              then (a19,e19) // (o9,c39) by A50, A72, AFF_1: 31;

              then (c39,a39) // (o9,c39) by A68, A69, AFF_1: 5;

              then (c39,o9) // (c39,a39) by AFF_1: 4;

              then LIN (c39,o9,a39) by AFF_1:def 1;

              then a39 in A9 by A50, A51, A65, A70, AFF_1: 25;

              then A9 // M9 by A5, A8, A9, A14, A21, A50, A51, A73, AFF_1: 38;

              then A // M by ANALMETR: 46;

              hence contradiction by A23, A56, ANALMETR: 52;

            end;

            then

            consider c19 be Element of the AffinStruct of X such that

             A74: c19 in A9 and

             A75: LIN (a19,e19,c19) by A50, AFF_1: 59;

            reconsider c1 = c19 as Element of X;

            reconsider c3 = c39 as Element of X;

            (a19,e19) // (a19,c19) by A75, AFF_1:def 1;

            then

             A76: (c39,a39) // (a19,c19) by A68, A69, AFF_1: 5;

            then

             A77: (c3,a3) // (a1,c1) by ANALMETR: 36;

            consider e19 be Element of the AffinStruct of X such that

             A78: (c39,a39) // (a29,e19) and

             A79: a29 <> e19 by DIRAF: 40;

             not (a29,e19) // A9

            proof

              

               A80: c39 <> o9

              proof

                assume c39 = o9;

                then

                 A81: (a3,b3) // (b2,o) by A67, ANALMETR: 36;

                (b29,o9) // (b29,b39) by A9, A11, A12, A22, AFF_1: 39, AFF_1: 41;

                then (b2,o) // (b2,b3) by ANALMETR: 36;

                then (a3,b3) // (b2,b3) by A5, A13, A81, ANALMETR: 60;

                then (b3,b2) // (b3,a3) by ANALMETR: 59;

                then LIN (b3,b2,a3) by ANALMETR:def 10;

                then LIN (b39,b29,a39) by ANALMETR: 40;

                hence contradiction by A11, A12, A14, A22, A28, AFF_1: 25;

              end;

              assume

               A82: (a29,e19) // A9;

              

               A83: (o9,a39) // (o9,a39) by AFF_1: 2;

              (o9,c39) // A9 by A50, A51, A65, AFF_1: 40, AFF_1: 41;

              then (a29,e19) // (o9,c39) by A50, A82, AFF_1: 31;

              then (c39,a39) // (o9,c39) by A78, A79, AFF_1: 5;

              then (c39,o9) // (c39,a39) by AFF_1: 4;

              then LIN (c39,o9,a39) by AFF_1:def 1;

              then a39 in A9 by A50, A51, A65, A80, AFF_1: 25;

              then A9 // M9 by A5, A8, A9, A14, A21, A50, A51, A83, AFF_1: 38;

              then A // M by ANALMETR: 46;

              hence contradiction by A23, A56, ANALMETR: 52;

            end;

            then

            consider c29 be Element of the AffinStruct of X such that

             A84: c29 in A9 and

             A85: LIN (a29,e19,c29) by A50, AFF_1: 59;

            reconsider c2 = c29 as Element of X;

            (a29,e19) // (a29,c29) by A85, AFF_1:def 1;

            then

             A86: (c39,a39) // (a29,c29) by A78, A79, AFF_1: 5;

            then

             A87: (c3,a3) // (a2,c2) by ANALMETR: 36;

            

             A88: o <> c3 & o <> c2 & o <> c1

            proof

               A89:

              now

                assume

                 A90: o = c3;

                (b29,o9) // (b39,b29) by A9, A11, A12, A22, AFF_1: 39, AFF_1: 41;

                then (a39,b39) // (b39,b29) by A5, A13, A67, A90, AFF_1: 5;

                then (b39,b29) // (b39,a39) by AFF_1: 4;

                then LIN (b39,b29,a39) by AFF_1:def 1;

                hence contradiction by A11, A12, A14, A22, A28, AFF_1: 25;

              end;

               A91:

              now

                (a19,o9) // (a19,a39) by A5, A6, A8, A21, AFF_1: 39, AFF_1: 41;

                then

                 A92: (a1,o) // (a1,a3) by ANALMETR: 36;

                assume o = c2 or o = c1;

                then

                 A93: (c3,a3) // (a1,o) or (c3,a3) // (a2,o) by A76, A86, ANALMETR: 36;

                (a29,o9) // (a19,a39) by A5, A6, A7, A8, A21, AFF_1: 39, AFF_1: 41;

                then (a2,o) // (a1,a3) by ANALMETR: 36;

                then (c3,a3) // (a1,a3) by A15, A16, A93, A92, ANALMETR: 60;

                then (a3,a1) // (a3,c3) by ANALMETR: 59;

                then LIN (a3,a1,c3) by ANALMETR:def 10;

                then LIN (a39,a19,c39) by ANALMETR: 40;

                then

                 A94: c39 in M9 by A6, A8, A21, A27, AFF_1: 25;

                (o9,c39) // (o9,c39) by AFF_1: 2;

                then A9 // M9 by A5, A21, A50, A51, A65, A89, A94, AFF_1: 38;

                then A // M by ANALMETR: 46;

                hence contradiction by A23, A56, ANALMETR: 52;

              end;

              assume o = c3 or o = c2 or o = c1;

              hence contradiction by A89, A91;

            end;

            

             A95: not c3 in N

            proof

              

               A96: (o9,c39) // (o9,c39) by AFF_1: 2;

              assume c3 in N;

              then A9 // N9 by A9, A22, A50, A51, A65, A88, A96, AFF_1: 38;

              then A // N by ANALMETR: 46;

              hence contradiction by A56, ANALMETR: 52;

            end;

            

             A97: not LIN (a3,a2,c3)

            proof

              assume LIN (a3,a2,c3);

              then LIN (a39,a29,c39) by ANALMETR: 40;

              then

               A98: c39 in M9 by A7, A8, A21, A26, AFF_1: 25;

              (o9,c39) // (o9,c39) by AFF_1: 2;

              then A9 // M9 by A5, A21, A50, A51, A65, A88, A98, AFF_1: 38;

              then A // M by ANALMETR: 46;

              hence contradiction by A23, A56, ANALMETR: 52;

            end;

            

             A99: not LIN (a3,a1,c3)

            proof

              assume LIN (a3,a1,c3);

              then LIN (a39,a19,c39) by ANALMETR: 40;

              then

               A100: c39 in M9 by A6, A8, A21, A27, AFF_1: 25;

              (o9,c39) // (o9,c39) by AFF_1: 2;

              then A9 // M9 by A5, A21, A50, A51, A65, A88, A100, AFF_1: 38;

              then A // M by ANALMETR: 46;

              hence contradiction by A23, A56, ANALMETR: 52;

            end;

            

             A101: not LIN (a1,a2,c1)

            proof

              assume LIN (a1,a2,c1);

              then LIN (a19,a29,c19) by ANALMETR: 40;

              then

               A102: c19 in M9 by A6, A7, A21, A25, AFF_1: 25;

              (o9,c19) // (o9,c19) by AFF_1: 2;

              then M9 // A9 by A5, A21, A50, A51, A74, A88, A102, AFF_1: 38;

              then M // A by ANALMETR: 46;

              hence contradiction by A23, A56, ANALMETR: 52;

            end;

            (o9,a19) // (o9,a29) by A5, A6, A7, A21, AFF_1: 39, AFF_1: 41;

            then LIN (o9,a19,a29) by AFF_1:def 1;

            then

             A103: LIN (o,a1,a2) by ANALMETR: 40;

            (o9,b29) // (o9,b19) by A9, A10, A11, A22, AFF_1: 39, AFF_1: 41;

            then LIN (o9,b29,b19) by AFF_1:def 1;

            then

             A104: LIN (o,b2,b1) by ANALMETR: 40;

            (o9,c19) // (o9,c29) by A50, A51, A74, A84, AFF_1: 39, AFF_1: 41;

            then LIN (o9,c19,c29) by AFF_1:def 1;

            then

             A105: LIN (o,c1,c2) by ANALMETR: 40;

            (o9,c39) // (o9,c29) by A50, A51, A65, A84, AFF_1: 39, AFF_1: 41;

            then LIN (o9,c39,c29) by AFF_1:def 1;

            then

             A106: LIN (o,c3,c2) by ANALMETR: 40;

            (o9,c39) // (o9,c19) by A50, A51, A65, A74, AFF_1: 39, AFF_1: 41;

            then LIN (o9,c39,c19) by AFF_1:def 1;

            then

             A107: LIN (o,c3,c1) by ANALMETR: 40;

            c3 <> a3

            proof

              

               A108: (o9,a39) // (o9,a39) by AFF_1: 2;

              assume c3 = a3;

              then A9 // M9 by A5, A8, A9, A14, A21, A50, A51, A65, A108, AFF_1: 38;

              then A // M by ANALMETR: 46;

              hence contradiction by A23, A56, ANALMETR: 52;

            end;

            then (a1,c1) // (a2,c2) by A77, A87, ANALMETR: 60;

            then

             A109: (c1,a1) // (c2,a2) by ANALMETR: 59;

            

             A110: not LIN (c1,c2,b2)

            proof

              

               A111: c19 <> c29

              proof

                

                 A112: c3 <> a3

                proof

                  

                   A113: (o9,c39) // (o9,c39) by AFF_1: 2;

                  assume c3 = a3;

                  then A9 // M9 by A5, A8, A9, A14, A21, A50, A51, A65, A113, AFF_1: 38;

                  then A // M by ANALMETR: 46;

                  hence contradiction by A23, A56, ANALMETR: 52;

                end;

                assume c19 = c29;

                then (a1,c1) // (a2,c1) by A77, A87, A112, ANALMETR: 60;

                then (c1,a2) // (c1,a1) by ANALMETR: 59;

                then LIN (c1,a2,a1) by ANALMETR:def 10;

                then LIN (c19,a29,a19) by ANALMETR: 40;

                then LIN (a19,a29,c19) by AFF_1: 6;

                then

                 A114: c19 in M9 by A6, A7, A21, A25, AFF_1: 25;

                (o9,c19) // (o9,c19) by AFF_1: 2;

                then A9 // M9 by A5, A21, A50, A51, A74, A88, A114, AFF_1: 38;

                then A // M by ANALMETR: 46;

                hence contradiction by A23, A56, ANALMETR: 52;

              end;

              assume LIN (c1,c2,b2);

              then LIN (c19,c29,b29) by ANALMETR: 40;

              then b29 in A9 by A50, A74, A84, A111, AFF_1: 25;

              then A9 = N9 by A5, A9, A11, A13, A22, A50, A51, AFF_1: 18;

              then A9 // N9 by A22, AFF_1: 41;

              then A // N by ANALMETR: 46;

              hence contradiction by A56, ANALMETR: 52;

            end;

            (o9,a39) // (o9,a29) by A5, A7, A8, A21, AFF_1: 39, AFF_1: 41;

            then LIN (o9,a39,a29) by AFF_1:def 1;

            then

             A115: LIN (o,a3,a2) by ANALMETR: 40;

            (o9,b39) // (o9,b19) by A9, A10, A12, A22, AFF_1: 39, AFF_1: 41;

            then LIN (o9,b39,b19) by AFF_1:def 1;

            then

             A116: LIN (o,b3,b1) by ANALMETR: 40;

            (a3,c3) // (a1,c1) by A77, ANALMETR: 59;

            then (b3,c3) // (b1,c1) by A2, A9, A14, A15, A17, A18, A20, A88, A99, A41, A44, A116, A107, CONAFFM:def 1;

            then

             A117: (c3,b3) // (c1,b1) by ANALMETR: 59;

            (a3,c3) // (a2,c2) by A87, ANALMETR: 59;

            then (b2,c3) // (b1,c2) by A2, A5, A9, A13, A14, A16, A17, A19, A88, A115, A104, A106, A43, A97, CONAFFM:def 1;

            then (c3,b2) // (c2,b1) by ANALMETR: 59;

            then (c1,b2) // (c2,b3) by A1, A9, A10, A11, A12, A17, A18, A51, A56, A65, A74, A84, A88, A117, A57, A95;

            hence thesis by A2, A5, A13, A15, A16, A18, A88, A103, A42, A105, A101, A110, A109, CONAFFM:def 1;

          end;

          now

            (o9,a19) // (o9,a29) by A5, A6, A7, A21, AFF_1: 39, AFF_1: 41;

            then LIN (o9,a19,a29) by AFF_1:def 1;

            then

             A118: LIN (o,a1,a2) by ANALMETR: 40;

            (o9,b29) // (o9,b19) by A9, A10, A11, A22, AFF_1: 39, AFF_1: 41;

            then LIN (o9,b29,b19) by AFF_1:def 1;

            then

             A119: LIN (o,b2,b1) by ANALMETR: 40;

            (o9,b29) // (o9,b39) by A9, A11, A12, A22, AFF_1: 39, AFF_1: 41;

            then LIN (o9,b29,b39) by AFF_1:def 1;

            then

             A120: LIN (o,b2,b3) by ANALMETR: 40;

            

             A121: not LIN (b3,b1,a3) & not LIN (b2,b1,a3)

            proof

              assume LIN (b3,b1,a3) or LIN (b2,b1,a3);

              then LIN (b39,b19,a39) or LIN (b29,b19,a39) by ANALMETR: 40;

              hence contradiction by A10, A11, A12, A14, A22, A28, AFF_1: 25;

            end;

            (o9,a39) // (o9,a29) by A5, A7, A8, A21, AFF_1: 39, AFF_1: 41;

            then LIN (o9,a39,a29) by AFF_1:def 1;

            then

             A122: LIN (o,a3,a2) by ANALMETR: 40;

            (o9,b39) // (o9,b19) by A9, A10, A12, A22, AFF_1: 39, AFF_1: 41;

            then LIN (o9,b39,b19) by AFF_1:def 1;

            then

             A123: LIN (o,b3,b1) by ANALMETR: 40;

            (o9,a39) // (o9,a19) by A5, A6, A8, A21, AFF_1: 39, AFF_1: 41;

            then LIN (o9,a39,a19) by AFF_1:def 1;

            then

             A124: LIN (o,a3,a1) by ANALMETR: 40;

            consider x be Element of X such that

             A125: (o,b2) _|_ (o,x) and

             A126: o <> x by ANALMETR: 39;

            

             A127: (o,x) _|_ N by A4, A5, A9, A11, A13, A125, ANALMETR: 55;

            consider e19 be Element of the AffinStruct of X such that

             A128: (a39,b29) // (b39,e19) and

             A129: b39 <> e19 by DIRAF: 40;

            reconsider x9 = x as Element of the AffinStruct of X;

             LIN (o9,x9,x9) by AFF_1: 7;

            then

            consider A9 be Subset of the AffinStruct of X such that

             A130: A9 is being_line and

             A131: o9 in A9 and

             A132: x9 in A9 and x9 in A9 by AFF_1: 21;

            reconsider A = A9 as Subset of X;

            

             A133: for e1 holds e1 in A implies LIN (o,x,e1)

            proof

              let e1 such that

               A134: e1 in A;

              reconsider e19 = e1 as Element of the AffinStruct of X;

              (o9,x9) // (o9,e19) by A130, A131, A132, A134, AFF_1: 39, AFF_1: 41;

              then LIN (o9,x9,e19) by AFF_1:def 1;

              hence thesis by ANALMETR: 40;

            end;

            for e1 holds LIN (o,x,e1) implies e1 in A

            proof

              let e1 such that

               A135: LIN (o,x,e1);

              reconsider e19 = e1 as Element of the AffinStruct of X;

               LIN (o9,x9,e19) by A135, ANALMETR: 40;

              hence thesis by A126, A130, A131, A132, AFF_1: 25;

            end;

            then A = ( Line (o,x)) by A133, ANALMETR:def 11;

            then

             A136: A _|_ N by A126, A127, ANALMETR:def 14;

            assume

             A137: (a3,b3) _|_ (o,b2);

             not (b39,e19) // A9

            proof

              assume

               A138: (b39,e19) // A9;

              consider d19,d29 be Element of the AffinStruct of X such that

               A139: d19 <> d29 and

               A140: A9 = ( Line (d19,d29)) by A130, AFF_1:def 3;

              

               A141: d29 in A9 by A140, AFF_1: 15;

              reconsider d1 = d19, d2 = d29 as Element of X;

              (d19,d29) // (d19,d29) by AFF_1: 2;

              then (d19,d29) // A9 by A139, A140, AFF_1:def 4;

              then (b39,e19) // (d19,d29) by A130, A138, AFF_1: 31;

              then (a39,b29) // (d19,d29) by A128, A129, AFF_1: 5;

              then

               A142: (a3,b2) // (d1,d2) by ANALMETR: 36;

              d19 in A9 by A140, AFF_1: 15;

              then (d1,d2) _|_ (o,b2) by A9, A11, A136, A141, ANALMETR: 56;

              then (a3,b2) _|_ (o,b2) by A139, A142, ANALMETR: 62;

              then (a3,b2) // (a3,b3) by A5, A13, A137, ANALMETR: 63;

              then LIN (a3,b2,b3) by ANALMETR:def 10;

              then LIN (a39,b29,b39) by ANALMETR: 40;

              then LIN (b29,b39,a39) by AFF_1: 6;

              hence contradiction by A11, A12, A14, A22, A28, AFF_1: 25;

            end;

            then

            consider c39 be Element of the AffinStruct of X such that

             A143: c39 in A9 and

             A144: LIN (b39,e19,c39) by A130, AFF_1: 59;

            

             A145: (b39,e19) // (b39,c39) by A144, AFF_1:def 1;

            consider e19 be Element of the AffinStruct of X such that

             A146: (c39,a39) // (a29,e19) and

             A147: a29 <> e19 by DIRAF: 40;

             not (a29,e19) // A9

            proof

              

               A148: c39 <> o9

              proof

                assume c39 = o9;

                then

                 A149: (a39,b29) // (b39,o9) by A128, A129, A145, AFF_1: 5;

                (b39,o9) // (b39,b29) by A9, A11, A12, A22, AFF_1: 39, AFF_1: 41;

                then (a39,b29) // (b39,b29) by A18, A149, AFF_1: 5;

                then (b29,b39) // (b29,a39) by AFF_1: 4;

                then LIN (b29,b39,a39) by AFF_1:def 1;

                hence contradiction by A11, A12, A14, A22, A28, AFF_1: 25;

              end;

              assume

               A150: (a29,e19) // A9;

              

               A151: (o9,a39) // (o9,a39) by AFF_1: 2;

              (o9,c39) // A9 by A130, A131, A143, AFF_1: 40, AFF_1: 41;

              then (a29,e19) // (o9,c39) by A130, A150, AFF_1: 31;

              then (c39,a39) // (o9,c39) by A146, A147, AFF_1: 5;

              then (c39,o9) // (c39,a39) by AFF_1: 4;

              then LIN (c39,o9,a39) by AFF_1:def 1;

              then a39 in A9 by A130, A131, A143, A148, AFF_1: 25;

              then A9 // M9 by A5, A8, A9, A14, A21, A130, A131, A151, AFF_1: 38;

              then A // M by ANALMETR: 46;

              hence contradiction by A23, A136, ANALMETR: 52;

            end;

            then

            consider c29 be Element of the AffinStruct of X such that

             A152: c29 in A9 and

             A153: LIN (a29,e19,c29) by A130, AFF_1: 59;

            reconsider c3 = c39 as Element of X;

            reconsider c2 = c29 as Element of X;

            (a29,e19) // (a29,c29) by A153, AFF_1:def 1;

            then (c39,a39) // (a29,c29) by A146, A147, AFF_1: 5;

            then

             A154: (c3,a3) // (a2,c2) by ANALMETR: 36;

            then

             A155: (a3,c3) // (a2,c2) by ANALMETR: 59;

            consider e19 be Element of the AffinStruct of X such that

             A156: (c39,a39) // (a19,e19) and

             A157: a19 <> e19 by DIRAF: 40;

             not (a19,e19) // A9

            proof

              

               A158: c39 <> o9

              proof

                assume c39 = o9;

                then

                 A159: (a39,b29) // (b39,o9) by A128, A129, A145, AFF_1: 5;

                (b39,o9) // (b39,b29) by A9, A11, A12, A22, AFF_1: 39, AFF_1: 41;

                then (a39,b29) // (b39,b29) by A18, A159, AFF_1: 5;

                then (b29,b39) // (b29,a39) by AFF_1: 4;

                then LIN (b29,b39,a39) by AFF_1:def 1;

                hence contradiction by A11, A12, A14, A22, A28, AFF_1: 25;

              end;

              assume

               A160: (a19,e19) // A9;

              

               A161: (o9,a39) // (o9,a39) by AFF_1: 2;

              (o9,c39) // A9 by A130, A131, A143, AFF_1: 40, AFF_1: 41;

              then (a19,e19) // (o9,c39) by A130, A160, AFF_1: 31;

              then (c39,a39) // (o9,c39) by A156, A157, AFF_1: 5;

              then (c39,o9) // (c39,a39) by AFF_1: 4;

              then LIN (c39,o9,a39) by AFF_1:def 1;

              then a39 in A9 by A130, A131, A143, A158, AFF_1: 25;

              then A9 // M9 by A5, A8, A9, A14, A21, A130, A131, A161, AFF_1: 38;

              then A // M by ANALMETR: 46;

              hence contradiction by A23, A136, ANALMETR: 52;

            end;

            then

            consider c19 be Element of the AffinStruct of X such that

             A162: c19 in A9 and

             A163: LIN (a19,e19,c19) by A130, AFF_1: 59;

            reconsider c1 = c19 as Element of X;

            (a19,e19) // (a19,c19) by A163, AFF_1:def 1;

            then (c39,a39) // (a19,c19) by A156, A157, AFF_1: 5;

            then

             A164: (c3,a3) // (a1,c1) by ANALMETR: 36;

            then

             A165: (a3,c3) // (a1,c1) by ANALMETR: 59;

            

             A166: (a39,b29) // (b39,c39) by A128, A129, A145, AFF_1: 5;

            

             A167: o <> c3 & o <> c2 & o <> c1

            proof

               A168:

              now

                assume o = c3;

                then

                 A169: (a3,b2) // (b3,o) by A166, ANALMETR: 36;

                (b39,o9) // (b29,b39) by A9, A11, A12, A22, AFF_1: 39, AFF_1: 41;

                then (b3,o) // (b2,b3) by ANALMETR: 36;

                then (a3,b2) // (b2,b3) by A18, A169, ANALMETR: 60;

                then (b2,b3) // (b2,a3) by ANALMETR: 59;

                then LIN (b2,b3,a3) by ANALMETR:def 10;

                then LIN (b29,b39,a39) by ANALMETR: 40;

                hence contradiction by A11, A12, A14, A22, A28, AFF_1: 25;

              end;

               A170:

              now

                (a29,o9) // (a29,a39) by A5, A7, A8, A21, AFF_1: 39, AFF_1: 41;

                then

                 A171: (a2,o) // (a2,a3) by ANALMETR: 36;

                assume o = c2 or o = c1;

                then

                 A172: (a3,c3) // (a2,o) or (a3,c3) // (a1,o) by A154, A164, ANALMETR: 59;

                (a19,o9) // (a29,a39) by A5, A6, A7, A8, A21, AFF_1: 39, AFF_1: 41;

                then (a1,o) // (a2,a3) by ANALMETR: 36;

                then (a3,c3) // (a2,a3) by A15, A16, A172, A171, ANALMETR: 60;

                then (a3,a2) // (a3,c3) by ANALMETR: 59;

                then LIN (a3,a2,c3) by ANALMETR:def 10;

                then LIN (a39,a29,c39) by ANALMETR: 40;

                then

                 A173: c39 in M9 by A7, A8, A21, A26, AFF_1: 25;

                (o9,c39) // (o9,c39) by AFF_1: 2;

                then A9 // M9 by A5, A21, A130, A131, A143, A168, A173, AFF_1: 38;

                then A // M by ANALMETR: 46;

                hence contradiction by A23, A136, ANALMETR: 52;

              end;

              assume o = c3 or o = c2 or o = c1;

              hence contradiction by A168, A170;

            end;

            

             A174: not c3 in N

            proof

              

               A175: (o9,c39) // (o9,c39) by AFF_1: 2;

              assume c3 in N;

              then A9 // N9 by A9, A22, A130, A131, A143, A167, A175, AFF_1: 38;

              then A // N by ANALMETR: 46;

              hence contradiction by A136, ANALMETR: 52;

            end;

            

             A176: not LIN (a1,a2,c1)

            proof

              assume LIN (a1,a2,c1);

              then LIN (a19,a29,c19) by ANALMETR: 40;

              then

               A177: c19 in M9 by A6, A7, A21, A25, AFF_1: 25;

              (o9,c19) // (o9,c19) by AFF_1: 2;

              then A9 // M9 by A5, A21, A130, A131, A162, A167, A177, AFF_1: 38;

              then A // M by ANALMETR: 46;

              hence contradiction by A23, A136, ANALMETR: 52;

            end;

            

             A178: not LIN (a3,a1,c3) & not LIN (a3,a2,c3)

            proof

              assume LIN (a3,a1,c3) or LIN (a3,a2,c3);

              then LIN (a39,a19,c39) or LIN (a39,a29,c39) by ANALMETR: 40;

              then

               A179: c39 in M9 or c39 in M9 by A6, A7, A8, A21, A26, A27, AFF_1: 25;

              (o9,c39) // (o9,c39) by AFF_1: 2;

              then A9 // M9 by A5, A21, A130, A131, A143, A167, A179, AFF_1: 38;

              then A // M by ANALMETR: 46;

              hence contradiction by A23, A136, ANALMETR: 52;

            end;

            

             A180: not b2 in A

            proof

              

               A181: (o9,b29) // (o9,b29) by AFF_1: 2;

              assume b2 in A;

              then A9 // N9 by A5, A9, A11, A13, A22, A130, A131, A181, AFF_1: 38;

              then A // N by ANALMETR: 46;

              hence contradiction by A136, ANALMETR: 52;

            end;

            

             A182: not LIN (c1,c2,b2)

            proof

              

               A183: c19 <> c29

              proof

                

                 A184: a3 <> c3

                proof

                  

                   A185: (o9,c39) // (o9,c39) by AFF_1: 2;

                  assume a3 = c3;

                  then A9 // M9 by A5, A8, A9, A14, A21, A130, A131, A143, A185, AFF_1: 38;

                  then A // M by ANALMETR: 46;

                  hence contradiction by A23, A136, ANALMETR: 52;

                end;

                assume c19 = c29;

                then (a2,c1) // (a1,c1) by A155, A165, A184, ANALMETR: 60;

                then (c1,a1) // (c1,a2) by ANALMETR: 59;

                then LIN (c1,a1,a2) by ANALMETR:def 10;

                then LIN (c19,a19,a29) by ANALMETR: 40;

                then LIN (a19,a29,c19) by AFF_1: 6;

                then

                 A186: c19 in M9 by A6, A7, A21, A25, AFF_1: 25;

                (o9,c19) // (o9,c19) by AFF_1: 2;

                then A9 // M9 by A5, A21, A130, A131, A162, A167, A186, AFF_1: 38;

                then A // M by ANALMETR: 46;

                hence contradiction by A23, A136, ANALMETR: 52;

              end;

              assume LIN (c1,c2,b2);

              then LIN (c19,c29,b29) by ANALMETR: 40;

              hence contradiction by A130, A152, A162, A180, A183, AFF_1: 25;

            end;

            (o9,c19) // (o9,c29) by A130, A131, A152, A162, AFF_1: 39, AFF_1: 41;

            then LIN (o9,c19,c29) by AFF_1:def 1;

            then

             A187: LIN (o,c1,c2) by ANALMETR: 40;

            a3 <> c3

            proof

              

               A188: (o9,a39) // (o9,a39) by AFF_1: 2;

              assume a3 = c3;

              then A9 // M9 by A5, A8, A9, A14, A21, A130, A131, A143, A188, AFF_1: 38;

              then A // M by ANALMETR: 46;

              hence contradiction by A23, A136, ANALMETR: 52;

            end;

            then (a2,c2) // (a1,c1) by A155, A165, ANALMETR: 60;

            then

             A189: (c1,a1) // (c2,a2) by ANALMETR: 59;

            (o9,c39) // (o9,c19) by A130, A131, A143, A162, AFF_1: 39, AFF_1: 41;

            then LIN (o9,c39,c19) by AFF_1:def 1;

            then LIN (o,c3,c1) by ANALMETR: 40;

            then (b3,c3) // (b1,c1) by A2, A9, A14, A15, A17, A18, A20, A165, A167, A121, A178, A124, A123, CONAFFM:def 1;

            then

             A190: (c3,b3) // (c1,b1) by ANALMETR: 59;

            (o9,c39) // (o9,c29) by A130, A131, A143, A152, AFF_1: 39, AFF_1: 41;

            then LIN (o9,c39,c29) by AFF_1:def 1;

            then LIN (o,c3,c2) by ANALMETR: 40;

            then (b2,c3) // (b1,c2) by A2, A5, A9, A13, A14, A16, A17, A19, A155, A167, A121, A178, A122, A119, CONAFFM:def 1;

            then (c3,b2) // (c2,b1) by ANALMETR: 59;

            then (c1,b2) // (c2,b3) by A1, A9, A10, A11, A12, A17, A18, A131, A136, A143, A152, A162, A167, A190, A180, A174;

            hence thesis by A2, A5, A13, A15, A16, A18, A167, A118, A120, A187, A176, A182, A189, CONAFFM:def 1;

          end;

          hence thesis by A40;

        end;

         A191:

        now

          

           A192: not LIN (o9,a39,b39)

          proof

            assume LIN (o9,a39,b39);

            then LIN (o9,b39,a39) by AFF_1: 6;

            hence contradiction by A9, A12, A14, A18, A22, AFF_1: 25;

          end;

          (o9,b39) // (o9,b19) by A9, A10, A12, A22, AFF_1: 39, AFF_1: 41;

          then

           A193: LIN (o9,b39,b19) by AFF_1:def 1;

          assume

           A194: a1 = a3;

          then (a39,b39) // (a39,b19) by A20, ANALMETR: 36;

          hence thesis by A19, A194, A192, A193, AFF_1: 14;

        end;

         A195:

        now

          (o9,b29) // (o9,b39) by A9, A11, A12, A22, AFF_1: 39, AFF_1: 41;

          then

           A196: LIN (o9,b29,b39) by AFF_1:def 1;

          assume

           A197: a1 = a2;

          a1 <> b1

          proof

            (o9,a19) // (o9,a39) by A5, A6, A8, A21, AFF_1: 39, AFF_1: 41;

            then

             A198: LIN (o9,a19,a39) by AFF_1:def 1;

            assume a1 = b1;

            hence contradiction by A9, A10, A14, A15, A22, A198, AFF_1: 25;

          end;

          then (a3,b2) // (a3,b3) by A19, A20, A197, ANALMETR: 60;

          then (a39,b29) // (a39,b39) by ANALMETR: 36;

          then b29 = b39 by A5, A8, A9, A13, A14, A21, A196, AFF_1: 14, AFF_1: 25;

          then (a19,b29) // (a29,b39) by A197, AFF_1: 2;

          hence thesis by ANALMETR: 36;

        end;

        now

          (o9,b29) // (o9,b19) by A9, A10, A11, A22, AFF_1: 39, AFF_1: 41;

          then

           A199: LIN (o9,b29,b19) by AFF_1:def 1;

          assume

           A200: a2 = a3;

          then (a39,b29) // (a39,b19) by A19, ANALMETR: 36;

          then b29 = b19 by A5, A8, A9, A13, A14, A21, A199, AFF_1: 14, AFF_1: 25;

          hence thesis by A20, A200, ANALMETR: 59;

        end;

        hence thesis by A195, A191, A24;

      end;

      hence thesis by A1, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20;

    end;

    theorem :: CONMETR:14

    X is satisfying_MH1 & X is satisfying_MH2 implies X is satisfying_OPAP

    proof

      assume

       A1: X is satisfying_MH1;

      assume

       A2: X is satisfying_MH2;

      let o, a1, a2, a3, b1, b2, b3, M, N;

      assume that

       A3: o in M and

       A4: a1 in M and

       A5: a2 in M and

       A6: a3 in M and

       A7: o in N and

       A8: b1 in N and

       A9: b2 in N and

       A10: b3 in N and

       A11: not b2 in M and

       A12: not a3 in N and

       A13: M _|_ N and

       A14: o <> a1 and

       A15: o <> a2 and o <> a3 and

       A16: o <> b1 and o <> b2 and

       A17: o <> b3 and

       A18: (a3,b2) // (a2,b1) and

       A19: (a3,b3) // (a1,b1);

      reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, b19 = b1, b29 = b2, b39 = b3 as Element of the AffinStruct of X;

      reconsider M9 = M, N9 = N as Subset of the AffinStruct of X;

      N is being_line by A13, ANALMETR: 44;

      then

       A20: N9 is being_line by ANALMETR: 43;

      M is being_line by A13, ANALMETR: 44;

      then

       A21: M9 is being_line by ANALMETR: 43;

       A22:

      now

        consider e1 be Element of X such that

         A23: (o,a3) // (o,e1) and

         A24: o <> e1 by ANALMETR: 39;

        consider d1 such that

         A25: (o,b3) // (o,d1) and

         A26: o <> d1 by ANALMETR: 39;

        reconsider d19 = d1 as Element of the AffinStruct of X;

        consider e2 be Element of X such that

         A27: (a1,b3) _|_ (d1,e2) and

         A28: d1 <> e2 by ANALMETR: 39;

        reconsider e19 = e1, e29 = e2 as Element of the AffinStruct of X;

        assume that

         A29: a1 <> a2 and a2 <> a3 and

         A30: a1 <> a3;

        

         A31: LIN (o,b3,d1) by A25, ANALMETR:def 10;

        then

         A32: LIN (o9,b39,d19) by ANALMETR: 40;

        N is being_line by A13, ANALMETR: 44;

        then

         A33: N9 is being_line by ANALMETR: 43;

        then

         A34: (o9,b29) // (o9,b39) by A7, A9, A10, AFF_1: 39, AFF_1: 41;

        then (o,b2) // (o,b3) by ANALMETR: 36;

        then

         A35: LIN (o,b2,b3) by ANALMETR:def 10;

        

         A36: b2 <> b3

        proof

          

           A37: not LIN (o9,b19,a29)

          proof

            (o9,a29) // (o9,a39) by A3, A5, A6, A21, AFF_1: 39, AFF_1: 41;

            then

             A38: LIN (o9,a29,a39) by AFF_1:def 1;

            assume LIN (o9,b19,a29);

            then a29 in N9 by A7, A8, A16, A20, AFF_1: 25;

            hence contradiction by A7, A12, A15, A20, A38, AFF_1: 25;

          end;

          assume b2 = b3;

          then (a1,b1) // (a2,b1) by A6, A11, A18, A19, ANALMETR: 60;

          then (b1,a2) // (b1,a1) by ANALMETR: 59;

          then

           A39: (b19,a29) // (b19,a19) by ANALMETR: 36;

          (o9,a29) // (o9,a19) by A3, A4, A5, A21, AFF_1: 39, AFF_1: 41;

          then LIN (o9,a29,a19) by AFF_1:def 1;

          hence contradiction by A29, A37, A39, AFF_1: 14;

        end;

        

         A40: not LIN (b2,a3,b3)

        proof

          assume LIN (b2,a3,b3);

          then LIN (b29,a39,b39) by ANALMETR: 40;

          then LIN (b29,b39,a39) by AFF_1: 6;

          hence contradiction by A9, A10, A12, A36, A33, AFF_1: 25;

        end;

        

         A41: a3 <> b3

        proof

          assume a3 = b3;

          then LIN (b29,a39,b39) by AFF_1: 7;

          hence contradiction by A40, ANALMETR: 40;

        end;

        (b29,b39) // (b29,b19) by A8, A9, A10, A33, AFF_1: 39, AFF_1: 41;

        then (b2,b3) // (b2,b1) by ANALMETR: 36;

        then

         A42: LIN (b2,b3,b1) by ANALMETR:def 10;

        M is being_line by A13, ANALMETR: 44;

        then

         A43: M9 is being_line by ANALMETR: 43;

        then (o9,a39) // (o9,a19) by A3, A4, A6, AFF_1: 39, AFF_1: 41;

        then

         A44: (o,a3) // (o,a1) by ANALMETR: 36;

        then

         A45: LIN (o,a3,a1) by ANALMETR:def 10;

        

         A46: not LIN (a3,a1,b2)

        proof

          assume LIN (a3,a1,b2);

          then LIN (a39,a19,b29) by ANALMETR: 40;

          hence contradiction by A4, A6, A11, A30, A43, AFF_1: 25;

        end;

        

         A47: a3 <> b2

        proof

          assume a3 = b2;

          then LIN (a39,a19,b29) by AFF_1: 7;

          hence contradiction by A46, ANALMETR: 40;

        end;

        

         A48: (o,a3) _|_ (o,b3) by A3, A6, A7, A10, A13, ANALMETR: 56;

         not (o,e1) // (d1,e2)

        proof

          reconsider e19 = e1, e29 = e2 as Element of the AffinStruct of X;

          assume (o,e1) // (d1,e2);

          then (o9,e19) // (d19,e29) by ANALMETR: 36;

          then (d19,e29) // (o9,e19) by AFF_1: 4;

          then (d1,e2) // (o,e1) by ANALMETR: 36;

          then (o,e1) _|_ (a1,b3) by A27, A28, ANALMETR: 62;

          then (o,a3) _|_ (a1,b3) by A23, A24, ANALMETR: 62;

          then (o,b3) // (a1,b3) by A7, A12, A48, ANALMETR: 63;

          then (o9,b39) // (a19,b39) by ANALMETR: 36;

          then (b39,o9) // (b39,a19) by AFF_1: 4;

          then LIN (b39,o9,a19) by AFF_1:def 1;

          then LIN (o9,b39,a19) by AFF_1: 6;

          then

           A49: (o9,b39) // (o9,a19) by AFF_1:def 1;

           LIN (o9,b29,b39) by A35, ANALMETR: 40;

          then (o9,b29) // (o9,b39) by AFF_1:def 1;

          then (o9,b39) // (o9,b29) by AFF_1: 4;

          then (o9,a19) // (o9,b29) by A17, A49, DIRAF: 40;

          then LIN (o9,a19,b29) by AFF_1:def 1;

          then LIN (a19,o9,b29) by AFF_1: 6;

          then

           A50: (a19,o9) // (a19,b29) by AFF_1:def 1;

           LIN (o9,a39,a19) by A45, ANALMETR: 40;

          then LIN (a19,o9,a39) by AFF_1: 6;

          then (a19,o9) // (a19,a39) by AFF_1:def 1;

          then (a19,b29) // (a19,a39) by A14, A50, DIRAF: 40;

          then LIN (a19,b29,a39) by AFF_1:def 1;

          then LIN (a39,a19,b29) by AFF_1: 6;

          hence contradiction by A46, ANALMETR: 40;

        end;

        then not (o9,e19) // (d19,e29) by ANALMETR: 36;

        then

        consider d29 be Element of the AffinStruct of X such that

         A51: LIN (o9,e19,d29) and

         A52: LIN (d19,e29,d29) by AFF_1: 60;

        reconsider d2 = d29 as Element of X;

         LIN (d1,e2,d2) by A52, ANALMETR: 40;

        then

         A53: (d1,e2) // (d1,d2) by ANALMETR:def 10;

        then

         A54: (a1,b3) _|_ (d1,d2) by A27, A28, ANALMETR: 62;

        then

         A55: (d1,d2) _|_ (b3,a1) by ANALMETR: 61;

         LIN (o,e1,d2) by A51, ANALMETR: 40;

        then (o,e1) // (o,d2) by ANALMETR:def 10;

        then

         A56: (o,a3) // (o,d2) by A23, A24, ANALMETR: 60;

        then

         A57: LIN (o,a3,d2) by ANALMETR:def 10;

        then

         A58: LIN (o9,a39,d29) by ANALMETR: 40;

        consider e1 be Element of X such that

         A59: (o,b3) // (o,e1) and

         A60: o <> e1 by ANALMETR: 39;

        consider e2 be Element of X such that

         A61: (b3,a3) _|_ (d2,e2) and

         A62: d2 <> e2 by ANALMETR: 39;

        reconsider e19 = e1, e29 = e2 as Element of the AffinStruct of X;

         not (o,e1) // (d2,e2)

        proof

          reconsider e19 = e1, e29 = e2 as Element of the AffinStruct of X;

          assume (o,e1) // (d2,e2);

          then (o9,e19) // (d29,e29) by ANALMETR: 36;

          then (d29,e29) // (o9,e19) by AFF_1: 4;

          then (d2,e2) // (o,e1) by ANALMETR: 36;

          then (o,e1) _|_ (b3,a3) by A61, A62, ANALMETR: 62;

          then (o,b3) _|_ (b3,a3) by A59, A60, ANALMETR: 62;

          then (b3,a3) // (o,a3) by A17, A48, ANALMETR: 63;

          then (b39,a39) // (o9,a39) by ANALMETR: 36;

          then (a39,b39) // (a39,o9) by AFF_1: 4;

          then LIN (a39,b39,o9) by AFF_1:def 1;

          then LIN (b39,o9,a39) by AFF_1: 6;

          then

           A63: (b39,o9) // (b39,a39) by AFF_1:def 1;

           LIN (o9,b29,b39) by A35, ANALMETR: 40;

          then LIN (b39,o9,b29) by AFF_1: 6;

          then (b39,o9) // (b39,b29) by AFF_1:def 1;

          then (b39,a39) // (b39,b29) by A17, A63, DIRAF: 40;

          then LIN (b39,a39,b29) by AFF_1:def 1;

          then LIN (b29,a39,b39) by AFF_1: 6;

          hence contradiction by A40, ANALMETR: 40;

        end;

        then not (o9,e19) // (d29,e29) by ANALMETR: 36;

        then

        consider d39 be Element of the AffinStruct of X such that

         A64: LIN (o9,e19,d39) and

         A65: LIN (d29,e29,d39) by AFF_1: 60;

        reconsider d3 = d39 as Element of X;

         LIN (d2,e2,d3) by A65, ANALMETR: 40;

        then

         A66: (d2,e2) // (d2,d3) by ANALMETR:def 10;

        then

         A67: (b3,a3) _|_ (d2,d3) by A61, A62, ANALMETR: 62;

        then (d2,d3) _|_ (a3,b3) by ANALMETR: 61;

        then

         A68: (d2,d3) _|_ (a1,b1) by A19, A41, ANALMETR: 62;

         LIN (o,e1,d3) by A64, ANALMETR: 40;

        then (o,e1) // (o,d3) by ANALMETR:def 10;

        then

         A69: (o,b3) // (o,d3) by A59, A60, ANALMETR: 60;

        then

         A70: LIN (o,b3,d3) by ANALMETR:def 10;

        then

         A71: LIN (o9,b39,d39) by ANALMETR: 40;

        consider e2 be Element of X such that

         A72: (a3,b2) _|_ (d3,e2) and

         A73: d3 <> e2 by ANALMETR: 39;

        consider e1 be Element of X such that

         A74: (o,a3) // (o,e1) and

         A75: o <> e1 by ANALMETR: 39;

        reconsider e19 = e1, e29 = e2 as Element of the AffinStruct of X;

         not (o,e1) // (d3,e2)

        proof

          reconsider e19 = e1, e29 = e2 as Element of the AffinStruct of X;

           LIN (o9,b29,b39) by A35, ANALMETR: 40;

          then LIN (b29,o9,b39) by AFF_1: 6;

          then

           A76: (b29,o9) // (b29,b39) by AFF_1:def 1;

          assume (o,e1) // (d3,e2);

          then (o9,e19) // (d39,e29) by ANALMETR: 36;

          then (d39,e29) // (o9,e19) by AFF_1: 4;

          then (d3,e2) // (o,e1) by ANALMETR: 36;

          then (o,e1) _|_ (a3,b2) by A72, A73, ANALMETR: 62;

          then (o,a3) _|_ (a3,b2) by A74, A75, ANALMETR: 62;

          then

           A77: (o,b3) // (a3,b2) by A7, A12, A48, ANALMETR: 63;

           LIN (o9,b29,b39) by A35, ANALMETR: 40;

          then LIN (o9,b39,b29) by AFF_1: 6;

          then LIN (o,b3,b2) by ANALMETR: 40;

          then (o,b3) // (o,b2) by ANALMETR:def 10;

          then (o,b2) // (a3,b2) by A17, A77, ANALMETR: 60;

          then (o9,b29) // (a39,b29) by ANALMETR: 36;

          then (b29,o9) // (b29,a39) by AFF_1: 4;

          then (b29,a39) // (b29,b39) by A3, A11, A76, DIRAF: 40;

          then LIN (b29,a39,b39) by AFF_1:def 1;

          hence contradiction by A40, ANALMETR: 40;

        end;

        then not (o9,e19) // (d39,e29) by ANALMETR: 36;

        then

        consider d49 be Element of the AffinStruct of X such that

         A78: LIN (o9,e19,d49) and

         A79: LIN (d39,e29,d49) by AFF_1: 60;

        reconsider d4 = d49 as Element of X;

         LIN (d3,e2,d4) by A79, ANALMETR: 40;

        then

         A80: (d3,e2) // (d3,d4) by ANALMETR:def 10;

        then

         A81: (d3,d4) _|_ (a3,b2) by A72, A73, ANALMETR: 62;

         LIN (o,e1,d4) by A78, ANALMETR: 40;

        then (o,e1) // (o,d4) by ANALMETR:def 10;

        then

         A82: (o,a3) // (o,d4) by A74, A75, ANALMETR: 60;

        then

         A83: LIN (o,a3,d4) by ANALMETR:def 10;

        then

         A84: LIN (o9,a39,d49) by ANALMETR: 40;

        

         A85: (a3,b2) _|_ (d3,d4) by A72, A73, A80, ANALMETR: 62;

        then (d3,d4) _|_ (a2,b1) or a3 = b2 by A18, ANALMETR: 62;

        then

         A86: (d3,d4) _|_ (b1,a2) by A47, ANALMETR: 61;

        

         A87: d2 <> o

        proof

          (o,a3) _|_ (o,d1) by A17, A48, A25, ANALMETR: 62;

          then

           A88: (d1,o) _|_ (o,a3) by ANALMETR: 61;

          assume d2 = o;

          then (d1,o) _|_ (a1,b3) by A27, A28, A53, ANALMETR: 62;

          then (o,a3) // (a1,b3) by A26, A88, ANALMETR: 63;

          then (a1,b3) // (o,a1) by A7, A12, A44, ANALMETR: 60;

          then (a19,b39) // (o9,a19) by ANALMETR: 36;

          then (a19,b39) // (a19,o9) by AFF_1: 4;

          then LIN (a19,b39,o9) by AFF_1:def 1;

          then LIN (o9,b39,a19) by AFF_1: 6;

          then

           A89: (o9,b39) // (o9,a19) by AFF_1:def 1;

           LIN (o9,b29,b39) by A35, ANALMETR: 40;

          then LIN (o9,b39,b29) by AFF_1: 6;

          then (o9,b39) // (o9,b29) by AFF_1:def 1;

          then (o9,a19) // (o9,b29) by A17, A89, DIRAF: 40;

          then LIN (o9,a19,b29) by AFF_1:def 1;

          then LIN (a19,o9,b29) by AFF_1: 6;

          then

           A90: (a19,o9) // (a19,b29) by AFF_1:def 1;

           LIN (o9,a39,a19) by A45, ANALMETR: 40;

          then LIN (a19,o9,a39) by AFF_1: 6;

          then (a19,o9) // (a19,a39) by AFF_1:def 1;

          then (a19,b29) // (a19,a39) by A14, A90, DIRAF: 40;

          then LIN (a19,b29,a39) by AFF_1:def 1;

          then LIN (a39,a19,b29) by AFF_1: 6;

          hence contradiction by A46, ANALMETR: 40;

        end;

        

         A91: not LIN (d1,d2,d3)

        proof

          

           A92: d2 <> d3

          proof

            assume d2 = d3;

            then (o9,b39) // (o9,d29) by A69, ANALMETR: 36;

            then (o9,d29) // (o9,b39) by AFF_1: 4;

            then (o,d2) // (o,b3) by ANALMETR: 36;

            then (o,b3) // (o,a3) by A56, A87, ANALMETR: 60;

            then (o9,b39) // (o9,a39) by ANALMETR: 36;

            then LIN (o9,b39,a39) by AFF_1:def 1;

            then LIN (b39,o9,a39) by AFF_1: 6;

            then (b39,o9) // (b39,a39) by AFF_1:def 1;

            then

             A93: (b3,o) // (b3,a3) by ANALMETR: 36;

             LIN (o9,b29,b39) by A35, ANALMETR: 40;

            then LIN (b39,o9,b29) by AFF_1: 6;

            then (b39,o9) // (b39,b29) by AFF_1:def 1;

            then (b3,o) // (b3,b2) by ANALMETR: 36;

            then (b3,b2) // (b3,a3) by A17, A93, ANALMETR: 60;

            then LIN (b3,b2,a3) by ANALMETR:def 10;

            then LIN (b39,b29,a39) by ANALMETR: 40;

            then LIN (b29,a39,b39) by AFF_1: 6;

            hence contradiction by A40, ANALMETR: 40;

          end;

          

           A94: d1 <> d2

          proof

            assume d1 = d2;

            then (o9,a39) // (o9,d19) by A56, ANALMETR: 36;

            then (o9,d19) // (o9,a39) by AFF_1: 4;

            then (o,d1) // (o,a3) by ANALMETR: 36;

            then (o,b3) // (o,a3) by A25, A26, ANALMETR: 60;

            then (o9,b39) // (o9,a39) by ANALMETR: 36;

            then LIN (o9,b39,a39) by AFF_1:def 1;

            then LIN (b39,o9,a39) by AFF_1: 6;

            then (b39,o9) // (b39,a39) by AFF_1:def 1;

            then

             A95: (b3,o) // (b3,a3) by ANALMETR: 36;

             LIN (o9,b29,b39) by A35, ANALMETR: 40;

            then LIN (b39,o9,b29) by AFF_1: 6;

            then (b39,o9) // (b39,b29) by AFF_1:def 1;

            then (b3,o) // (b3,b2) by ANALMETR: 36;

            then (b3,b2) // (b3,a3) by A17, A95, ANALMETR: 60;

            then LIN (b3,b2,a3) by ANALMETR:def 10;

            then LIN (b39,b29,a39) by ANALMETR: 40;

            then LIN (b29,a39,b39) by AFF_1: 6;

            hence contradiction by A40, ANALMETR: 40;

          end;

          assume LIN (d1,d2,d3);

          then LIN (d19,d29,d39) by ANALMETR: 40;

          then LIN (d29,d19,d39) by AFF_1: 6;

          then (d29,d19) // (d29,d39) by AFF_1:def 1;

          then (d19,d29) // (d29,d39) by AFF_1: 4;

          then (d1,d2) // (d2,d3) by ANALMETR: 36;

          then (d2,d3) _|_ (a1,b3) by A54, A94, ANALMETR: 62;

          then (a1,b3) // (b3,a3) by A67, A92, ANALMETR: 63;

          then (a19,b39) // (b39,a39) by ANALMETR: 36;

          then (b39,a19) // (b39,a39) by AFF_1: 4;

          then LIN (b39,a19,a39) by AFF_1:def 1;

          then LIN (a19,a39,b39) by AFF_1: 6;

          then (a19,a39) // (a19,b39) by AFF_1:def 1;

          then

           A96: (a1,a3) // (a1,b3) by ANALMETR: 36;

          

           A97: a1 <> a3

          proof

            assume a1 = a3;

            then LIN (a39,a19,b29) by AFF_1: 7;

            hence contradiction by A46, ANALMETR: 40;

          end;

           LIN (o9,a39,a19) by A45, ANALMETR: 40;

          then LIN (a19,a39,o9) by AFF_1: 6;

          then (a19,a39) // (a19,o9) by AFF_1:def 1;

          then (a1,a3) // (a1,o) by ANALMETR: 36;

          then (a1,o) // (a1,b3) by A97, A96, ANALMETR: 60;

          then LIN (a1,o,b3) by ANALMETR:def 10;

          then LIN (a19,o9,b39) by ANALMETR: 40;

          then LIN (o9,b39,a19) by AFF_1: 6;

          then

           A98: (o9,b39) // (o9,a19) by AFF_1:def 1;

          (o9,b39) // (o9,b29) by A34, AFF_1: 4;

          then (o9,a19) // (o9,b29) by A17, A98, DIRAF: 40;

          then LIN (o9,a19,b29) by AFF_1:def 1;

          then LIN (a19,o9,b29) by AFF_1: 6;

          then (a19,o9) // (a19,b29) by AFF_1:def 1;

          then

           A99: (a1,o) // (a1,b2) by ANALMETR: 36;

           LIN (o9,a39,a19) by A45, ANALMETR: 40;

          then LIN (a19,o9,a39) by AFF_1: 6;

          then (a19,o9) // (a19,a39) by AFF_1:def 1;

          then (a1,o) // (a1,a3) by ANALMETR: 36;

          then (a1,b2) // (a1,a3) by A14, A99, ANALMETR: 60;

          then LIN (a1,b2,a3) by ANALMETR:def 10;

          then LIN (a19,b29,a39) by ANALMETR: 40;

          then LIN (a39,a19,b29) by AFF_1: 6;

          hence contradiction by A46, ANALMETR: 40;

        end;

        

         A100: d2 <> d4

        proof

          

           A101: d2 <> d3

          proof

            assume d2 = d3;

            then LIN (d19,d29,d39) by AFF_1: 7;

            hence contradiction by A91, ANALMETR: 40;

          end;

          assume d2 = d4;

          then (a3,b2) _|_ (d2,d3) by A85, ANALMETR: 61;

          then (a3,b2) // (b3,a3) by A67, A101, ANALMETR: 63;

          then (a3,b2) // (a3,b3) by ANALMETR: 59;

          then LIN (a3,b2,b3) by ANALMETR:def 10;

          then LIN (a39,b29,b39) by ANALMETR: 40;

          then LIN (b29,b39,a39) by AFF_1: 6;

          hence contradiction by A9, A10, A12, A20, A36, AFF_1: 25;

        end;

         LIN (o9,b39,b39) by AFF_1: 7;

        then

         A102: LIN (d19,d39,b39) by A17, A32, A71, AFF_1: 8;

        then

        consider A9 such that

         A103: A9 is being_line and

         A104: d19 in A9 and

         A105: d39 in A9 and

         A106: b39 in A9 by AFF_1: 21;

        reconsider A = A9 as Subset of X;

        

         A107: d19 <> d39

        proof

          assume d19 = d39;

          then LIN (d19,d29,d39) by AFF_1: 7;

          hence contradiction by A91, ANALMETR: 40;

        end;

        then A9 = ( Line (d19,d39)) by A103, A104, A105, AFF_1: 24;

        then

         A108: A = ( Line (d1,d3)) by ANALMETR: 41;

         LIN (o9,b29,b39) by A35, ANALMETR: 40;

        then

         A109: LIN (o9,b39,b29) by AFF_1: 6;

        then

         A110: b2 in A by A17, A32, A71, A103, A104, A105, A107, AFF_1: 8, AFF_1: 25;

        

         A111: o <> d3

        proof

          assume d3 = o;

          then

           A112: (d2,o) _|_ (b3,a3) by A61, A62, A66, ANALMETR: 62;

          (o,b3) _|_ (o,d2) by A7, A12, A48, A56, ANALMETR: 62;

          then (d2,o) _|_ (o,b3) by ANALMETR: 61;

          then (o,b3) // (b3,a3) by A87, A112, ANALMETR: 63;

          then (o9,b39) // (b39,a39) by ANALMETR: 36;

          then

           A113: (b39,o9) // (b39,a39) by AFF_1: 4;

           LIN (o9,b29,b39) by A35, ANALMETR: 40;

          then LIN (b39,o9,b29) by AFF_1: 6;

          then (b39,o9) // (b39,b29) by AFF_1:def 1;

          then (b39,a39) // (b39,b29) by A17, A113, DIRAF: 40;

          then LIN (b39,a39,b29) by AFF_1:def 1;

          then LIN (b29,a39,b39) by AFF_1: 6;

          hence contradiction by A40, ANALMETR: 40;

        end;

        

         A114: o <> d4

        proof

          (o,a3) _|_ (o,d3) by A17, A48, A69, ANALMETR: 62;

          then

           A115: (d3,o) _|_ (o,a3) by ANALMETR: 61;

          assume d4 = o;

          then (d3,o) _|_ (a3,b2) by A72, A73, A80, ANALMETR: 62;

          then (o,a3) // (a3,b2) by A111, A115, ANALMETR: 63;

          then (o9,a39) // (a39,b29) by ANALMETR: 36;

          then

           A116: (a39,o9) // (a39,b29) by AFF_1: 4;

           LIN (o9,a39,a19) by A45, ANALMETR: 40;

          then LIN (a39,o9,a19) by AFF_1: 6;

          then (a39,o9) // (a39,a19) by AFF_1:def 1;

          then (a39,b29) // (a39,a19) by A7, A12, A116, DIRAF: 40;

          then LIN (a39,b29,a19) by AFF_1:def 1;

          then LIN (a39,a19,b29) by AFF_1: 6;

          hence contradiction by A46, ANALMETR: 40;

        end;

        

         A117: not LIN (d1,d4,d3)

        proof

          

           A118: d1 <> d3

          proof

            

             A119: d1 <> d2

            proof

              assume d1 = d2;

              then (o9,a39) // (o9,d19) by A56, ANALMETR: 36;

              then (o9,d19) // (o9,a39) by AFF_1: 4;

              then (o,d1) // (o,a3) by ANALMETR: 36;

              then (o,b3) // (o,a3) by A25, A26, ANALMETR: 60;

              then (o9,b39) // (o9,a39) by ANALMETR: 36;

              then LIN (o9,b39,a39) by AFF_1:def 1;

              then LIN (b39,o9,a39) by AFF_1: 6;

              then (b39,o9) // (b39,a39) by AFF_1:def 1;

              then

               A120: (b3,o) // (b3,a3) by ANALMETR: 36;

               LIN (o9,b29,b39) by A35, ANALMETR: 40;

              then LIN (b39,o9,b29) by AFF_1: 6;

              then (b39,o9) // (b39,b29) by AFF_1:def 1;

              then (b3,o) // (b3,b2) by ANALMETR: 36;

              then (b3,b2) // (b3,a3) by A17, A120, ANALMETR: 60;

              then LIN (b3,b2,a3) by ANALMETR:def 10;

              then LIN (b39,b29,a39) by ANALMETR: 40;

              then LIN (b29,a39,b39) by AFF_1: 6;

              hence contradiction by A40, ANALMETR: 40;

            end;

            assume d1 = d3;

            then (a3,b3) _|_ (d1,d2) by A67, ANALMETR: 61;

            then (a1,b3) // (a3,b3) by A54, A119, ANALMETR: 63;

            then (a19,b39) // (a39,b39) by ANALMETR: 36;

            then (b39,a19) // (b39,a39) by AFF_1: 4;

            then LIN (b39,a19,a39) by AFF_1:def 1;

            then LIN (a19,a39,b39) by AFF_1: 6;

            then (a19,a39) // (a19,b39) by AFF_1:def 1;

            then

             A121: (a1,a3) // (a1,b3) by ANALMETR: 36;

            

             A122: a1 <> a3

            proof

              assume a1 = a3;

              then LIN (a39,a19,b29) by AFF_1: 7;

              hence contradiction by A46, ANALMETR: 40;

            end;

             LIN (o9,a39,a19) by A45, ANALMETR: 40;

            then LIN (a19,a39,o9) by AFF_1: 6;

            then (a19,a39) // (a19,o9) by AFF_1:def 1;

            then (a1,a3) // (a1,o) by ANALMETR: 36;

            then (a1,o) // (a1,b3) by A122, A121, ANALMETR: 60;

            then LIN (a1,o,b3) by ANALMETR:def 10;

            then LIN (a19,o9,b39) by ANALMETR: 40;

            then LIN (o9,b39,a19) by AFF_1: 6;

            then

             A123: (o9,b39) // (o9,a19) by AFF_1:def 1;

            (o9,b39) // (o9,b29) by A34, AFF_1: 4;

            then (o9,a19) // (o9,b29) by A17, A123, DIRAF: 40;

            then LIN (o9,a19,b29) by AFF_1:def 1;

            then LIN (a19,o9,b29) by AFF_1: 6;

            then (a19,o9) // (a19,b29) by AFF_1:def 1;

            then

             A124: (a1,o) // (a1,b2) by ANALMETR: 36;

             LIN (o9,a39,a19) by A45, ANALMETR: 40;

            then LIN (a19,o9,a39) by AFF_1: 6;

            then (a19,o9) // (a19,a39) by AFF_1:def 1;

            then (a1,o) // (a1,a3) by ANALMETR: 36;

            then (a1,b2) // (a1,a3) by A14, A124, ANALMETR: 60;

            then LIN (a1,b2,a3) by ANALMETR:def 10;

            then LIN (a19,b29,a39) by ANALMETR: 40;

            then LIN (a39,a19,b29) by AFF_1: 6;

            hence contradiction by A46, ANALMETR: 40;

          end;

          assume LIN (d1,d4,d3);

          then LIN (d19,d49,d39) by ANALMETR: 40;

          then

           A125: LIN (d19,d39,d49) by AFF_1: 6;

          

           A126: b29 <> b39

          proof

            assume b29 = b39;

            then LIN (b29,a39,b39) by AFF_1: 7;

            hence contradiction by A40, ANALMETR: 40;

          end;

           LIN (o9,b29,b39) by A35, ANALMETR: 40;

          then LIN (b29,b39,o9) by AFF_1: 6;

          then

           A127: (b29,b39) // (b29,o9) by AFF_1:def 1;

           LIN (d19,d39,b29) by A17, A32, A71, A109, AFF_1: 8;

          then LIN (b29,b39,d49) by A102, A118, A125, AFF_1: 8;

          then (b29,b39) // (b29,d49) by AFF_1:def 1;

          then (b29,o9) // (b29,d49) by A127, A126, DIRAF: 40;

          then LIN (b29,o9,d49) by AFF_1:def 1;

          then LIN (o9,d49,b29) by AFF_1: 6;

          then

           A128: (o9,d49) // (o9,b29) by AFF_1:def 1;

          (o9,a39) // (o9,d49) by A82, ANALMETR: 36;

          then (o9,d49) // (o9,a39) by AFF_1: 4;

          then (o9,b29) // (o9,a39) by A114, A128, DIRAF: 40;

          then LIN (o9,b29,a39) by AFF_1:def 1;

          then LIN (b29,o9,a39) by AFF_1: 6;

          then

           A129: (b29,o9) // (b29,a39) by AFF_1:def 1;

           LIN (o9,b29,b39) by A35, ANALMETR: 40;

          then LIN (b29,o9,b39) by AFF_1: 6;

          then (b29,o9) // (b29,b39) by AFF_1:def 1;

          then (b29,a39) // (b29,b39) by A3, A11, A129, DIRAF: 40;

          then LIN (b29,a39,b39) by AFF_1:def 1;

          hence contradiction by A40, ANALMETR: 40;

        end;

        

         A130: not d4 in A

        proof

          assume d4 in A;

          then (d19,d49) // (d19,d39) by A103, A104, A105, AFF_1: 39, AFF_1: 41;

          then LIN (d19,d49,d39) by AFF_1:def 1;

          hence contradiction by A117, ANALMETR: 40;

        end;

        

         A131: (d2,d3) _|_ (b3,a3) by A61, A62, A66, ANALMETR: 62;

        take d4;

         LIN (o9,b39,d19) by A31, ANALMETR: 40;

        then

         A132: (o9,b39) // (o9,d19) by AFF_1:def 1;

         LIN (o9,a39,a19) by A45, ANALMETR: 40;

        then

         A133: LIN (d29,d49,a19) by A7, A12, A58, A84, AFF_1: 8;

        then

        consider K9 such that

         A134: K9 is being_line and

         A135: d29 in K9 and

         A136: d49 in K9 and

         A137: a19 in K9 by AFF_1: 21;

        reconsider K = K9 as Subset of X;

         LIN (o9,a39,a39) by AFF_1: 7;

        then

         A138: a3 in K by A7, A12, A58, A84, A100, A134, A135, A136, AFF_1: 8, AFF_1: 25;

        (a39,a19) // (a39,a29) by A4, A5, A6, A43, AFF_1: 39, AFF_1: 41;

        then (a3,a1) // (a3,a2) by ANALMETR: 36;

        then

         A139: LIN (a3,a1,a2) by ANALMETR:def 10;

        

         A140: LIN (d1,d3,b3) & LIN (d1,d3,b1) & LIN (d2,d4,a1) & LIN (d2,d4,a2)

        proof

          

           A141: b39 <> b29

          proof

            assume b39 = b29;

            then LIN (b29,a39,b39) by AFF_1: 7;

            hence contradiction by A40, ANALMETR: 40;

          end;

           LIN (o9,b29,b39) by A35, ANALMETR: 40;

          then LIN (b39,b29,o9) by AFF_1: 6;

          then

           A142: (b39,b29) // (b39,o9) by AFF_1:def 1;

           LIN (b29,b39,b19) by A42, ANALMETR: 40;

          then LIN (b39,b29,b19) by AFF_1: 6;

          then (b39,b29) // (b39,b19) by AFF_1:def 1;

          then (b39,b19) // (b39,o9) by A142, A141, DIRAF: 40;

          then LIN (b39,b19,o9) by AFF_1:def 1;

          then

           A143: LIN (o9,b39,b19) by AFF_1: 6;

          

           A144: LIN (o9,b39,d39) by A70, ANALMETR: 40;

           LIN (o9,b39,d19) by A31, ANALMETR: 40;

          then

           A145: LIN (d19,d39,b19) by A17, A143, A144, AFF_1: 8;

          reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, d29 = d2, d49 = d4 as Element of the AffinStruct of X;

          

           A146: a39 <> a19

          proof

            assume a19 = a39;

            then LIN (a39,a19,b29) by AFF_1: 7;

            hence contradiction by A46, ANALMETR: 40;

          end;

           LIN (o9,a39,a19) by A45, ANALMETR: 40;

          then LIN (a39,a19,o9) by AFF_1: 6;

          then

           A147: (a39,a19) // (a39,o9) by AFF_1:def 1;

           LIN (a39,a19,a29) by A139, ANALMETR: 40;

          then (a39,a19) // (a39,a29) by AFF_1:def 1;

          then (a39,a29) // (a39,o9) by A147, A146, DIRAF: 40;

          then LIN (a39,a29,o9) by AFF_1:def 1;

          then

           A148: LIN (o9,a39,a29) by AFF_1: 6;

          

           A149: LIN (o9,a39,d49) by A83, ANALMETR: 40;

           LIN (o9,a39,d29) by A57, ANALMETR: 40;

          then LIN (d29,d49,a29) by A7, A12, A148, A149, AFF_1: 8;

          hence thesis by A102, A133, A145, ANALMETR: 40;

        end;

         LIN (o9,b39,d39) by A70, ANALMETR: 40;

        then (o9,b39) // (o9,d39) by AFF_1:def 1;

        then (o9,d19) // (o9,d39) by A17, A132, DIRAF: 40;

        then LIN (o9,d19,d39) by AFF_1:def 1;

        then LIN (d19,o9,d39) by AFF_1: 6;

        then (d19,o9) // (d19,d39) by AFF_1:def 1;

        then (o9,d19) // (d19,d39) by AFF_1: 4;

        then

         A150: (o,d1) // (d1,d3) by ANALMETR: 36;

        (o,b3) // (o,d1) by A132, ANALMETR: 36;

        then (o,d1) _|_ (o,a3) by A17, A48, ANALMETR: 62;

        then

         A151: (o,a3) _|_ (d1,d3) by A26, A150, ANALMETR: 62;

         LIN (o9,a39,d29) by A57, ANALMETR: 40;

        then

         A152: (o9,a39) // (o9,d29) by AFF_1:def 1;

        then (o,a3) // (o,d2) by ANALMETR: 36;

        then

         A153: (o,d2) _|_ (d1,d3) by A7, A12, A151, ANALMETR: 62;

        

         A154: not d2 in A

        proof

          assume d2 in A;

          then (d19,d29) // (d19,d39) by A103, A104, A105, AFF_1: 39, AFF_1: 41;

          then LIN (d19,d29,d39) by AFF_1:def 1;

          hence contradiction by A91, ANALMETR: 40;

        end;

         LIN (o9,a39,d49) by A83, ANALMETR: 40;

        then (o9,a39) // (o9,d49) by AFF_1:def 1;

        then (o9,d29) // (o9,d49) by A7, A12, A152, DIRAF: 40;

        then LIN (o9,d29,d49) by AFF_1:def 1;

        then LIN (d29,o9,d49) by AFF_1: 6;

        then (d29,o9) // (d29,d49) by AFF_1:def 1;

        then (o9,d29) // (d29,d49) by AFF_1: 4;

        then (o,d2) // (d2,d4) by ANALMETR: 36;

        then

         A155: (d1,d3) _|_ (d2,d4) by A87, A153, ANALMETR: 62;

        K9 = ( Line (d29,d49)) by A100, A134, A135, A136, AFF_1: 24;

        then K = ( Line (d2,d4)) by ANALMETR: 41;

        then

         A156: A _|_ K by A155, A100, A107, A108, ANALMETR: 45;

        reconsider d19 = d1, d29 = d2, d39 = d3, d49 = d4, b39 = b3, a19 = a1, b19 = b1, a29 = a2 as Element of the AffinStruct of X;

         LIN (d19,d39,b39) by A140, ANALMETR: 40;

        then

        consider A9 such that

         A157: A9 is being_line and

         A158: d19 in A9 and

         A159: d39 in A9 and

         A160: b39 in A9 by AFF_1: 21;

        

         A161: d19 <> d39

        proof

          assume d19 = d39;

          then LIN (d19,d29,d39) by AFF_1: 7;

          hence contradiction by A91, ANALMETR: 40;

        end;

        reconsider A = A9 as Subset of X;

         LIN (d19,d39,b19) by A140, ANALMETR: 40;

        then

         A162: b1 in A by A157, A158, A159, A161, AFF_1: 25;

        

         A163: not d2 in A

        proof

          assume d2 in A;

          then (d19,d29) // (d19,d39) by A157, A158, A159, AFF_1: 39, AFF_1: 41;

          then (d1,d2) // (d1,d3) by ANALMETR: 36;

          hence contradiction by A91, ANALMETR:def 10;

        end;

        

         A164: d1 <> d4

        proof

           LIN (o9,a39,d49) by A83, ANALMETR: 40;

          then

           A165: LIN (o9,d49,a39) by AFF_1: 6;

           LIN (o9,d49,o9) by AFF_1: 7;

          then

           A166: (o9,d49) // (o9,a39) by A165, AFF_1: 10;

          

           A167: LIN (o9,b39,o9) by AFF_1: 7;

           LIN (o9,b29,b39) by A35, ANALMETR: 40;

          then

           A168: LIN (o9,b39,b29) by AFF_1: 6;

           LIN (o9,b39,d19) by A31, ANALMETR: 40;

          then LIN (o9,d19,b29) by A17, A167, A168, AFF_1: 8;

          then

           A169: (o9,d19) // (o9,b29) by AFF_1:def 1;

          assume d1 = d4;

          then (o9,a39) // (o9,b29) by A114, A169, A166, DIRAF: 40;

          then LIN (o9,a39,b29) by AFF_1:def 1;

          then LIN (a39,b29,o9) by AFF_1: 6;

          then (a39,b29) // (a39,o9) by AFF_1:def 1;

          then

           A170: (a39,o9) // (a39,b29) by AFF_1: 4;

           LIN (o9,a39,a19) by A45, ANALMETR: 40;

          then LIN (a39,o9,a19) by AFF_1: 6;

          then (a39,o9) // (a39,a19) by AFF_1:def 1;

          then (a39,b29) // (a39,a19) by A7, A12, A170, DIRAF: 40;

          then LIN (a39,b29,a19) by AFF_1:def 1;

          then LIN (a39,a19,b29) by AFF_1: 6;

          hence contradiction by A46, ANALMETR: 40;

        end;

        

         A171: not d4 in A

        proof

          assume d4 in A;

          then (d19,d49) // (d19,d39) by A157, A158, A159, AFF_1: 39, AFF_1: 41;

          then (d1,d4) // (d1,d3) by ANALMETR: 36;

          hence contradiction by A117, ANALMETR:def 10;

        end;

         LIN (d29,d49,a19) by A140, ANALMETR: 40;

        then

        consider K9 such that

         A172: K9 is being_line and

         A173: d29 in K9 and

         A174: d49 in K9 and

         A175: a19 in K9 by AFF_1: 21;

        reconsider K = K9 as Subset of X;

         LIN (d29,d49,a29) by A140, ANALMETR: 40;

        then

         A176: a2 in K by A100, A172, A173, A174, AFF_1: 25;

        K9 = ( Line (d29,d49)) by A100, A172, A173, A174, AFF_1: 24;

        then

         A177: K = ( Line (d2,d4)) by ANALMETR: 41;

        A9 = ( Line (d19,d39)) by A157, A158, A159, A161, AFF_1: 24;

        then A = ( Line (d1,d3)) by ANALMETR: 41;

        then A _|_ K by A155, A100, A161, A177, ANALMETR: 45;

        then

         A178: (d1,d4) _|_ (b3,a2) by A1, A68, A86, A55, A158, A159, A160, A173, A174, A175, A163, A171, A162, A176;

        (d1,d2) _|_ (a1,b3) by A27, A28, A53, ANALMETR: 62;

        then (d1,d4) _|_ (a1,b2) by A2, A131, A81, A104, A105, A106, A135, A136, A137, A154, A130, A156, A110, A138;

        then (a1,b2) // (b3,a2) or d1 = d4 by A178, ANALMETR: 63;

        then (a19,b29) // (b39,a29) by A164, ANALMETR: 36;

        then (a19,b29) // (a29,b39) by AFF_1: 4;

        hence thesis by ANALMETR: 36;

      end;

      now

         A179:

        now

          (o9,b29) // (o9,b39) by A7, A9, A10, A20, AFF_1: 39, AFF_1: 41;

          then

           A180: LIN (o9,b29,b39) by AFF_1:def 1;

          assume

           A181: a1 = a2;

          a1 <> b1

          proof

            (o9,a19) // (o9,a39) by A3, A4, A6, A21, AFF_1: 39, AFF_1: 41;

            then

             A182: LIN (o9,a19,a39) by AFF_1:def 1;

            assume a1 = b1;

            hence contradiction by A7, A8, A12, A14, A20, A182, AFF_1: 25;

          end;

          then (a3,b2) // (a3,b3) by A18, A19, A181, ANALMETR: 60;

          then (a39,b29) // (a39,b39) by ANALMETR: 36;

          then b29 = b39 by A3, A6, A7, A11, A12, A21, A180, AFF_1: 14, AFF_1: 25;

          then (a19,b29) // (a29,b39) by A181, AFF_1: 2;

          hence thesis by ANALMETR: 36;

        end;

         A183:

        now

          

           A184: not LIN (o9,a39,b19)

          proof

            assume LIN (o9,a39,b19);

            then LIN (o9,b19,a39) by AFF_1: 6;

            hence contradiction by A7, A8, A12, A16, A20, AFF_1: 25;

          end;

          (o9,b19) // (o9,b39) by A7, A8, A10, A20, AFF_1: 39, AFF_1: 41;

          then

           A185: LIN (o9,b19,b39) by AFF_1:def 1;

          assume

           A186: a1 = a3;

          then (a3,b1) // (a3,b3) by A19, ANALMETR: 59;

          then (a39,b19) // (a39,b39) by ANALMETR: 36;

          hence thesis by A18, A186, A184, A185, AFF_1: 14;

        end;

         A187:

        now

          

           A188: not LIN (o9,a39,b19)

          proof

            assume LIN (o9,a39,b19);

            then LIN (o9,b19,a39) by AFF_1: 6;

            hence contradiction by A7, A8, A12, A16, A20, AFF_1: 25;

          end;

          (o9,b19) // (o9,b29) by A7, A8, A9, A20, AFF_1: 39, AFF_1: 41;

          then

           A189: LIN (o9,b19,b29) by AFF_1:def 1;

          assume

           A190: a2 = a3;

          then (a3,b1) // (a3,b2) by A18, ANALMETR: 59;

          then (a39,b19) // (a39,b29) by ANALMETR: 36;

          then (a2,b3) // (a1,b2) by A19, A190, A188, A189, AFF_1: 14;

          hence thesis by ANALMETR: 59;

        end;

        assume a1 = a2 or a2 = a3 or a1 = a3;

        hence thesis by A179, A187, A183;

      end;

      hence thesis by A22;

    end;

    theorem :: CONMETR:15

    X is satisfying_3H implies X is satisfying_OPAP

    proof

      assume

       A1: X is satisfying_3H;

      let o, a1, a2, a3, b1, b2, b3, M, N;

      assume that

       A2: o in M and

       A3: a1 in M and

       A4: a2 in M and

       A5: a3 in M and

       A6: o in N and

       A7: b1 in N and

       A8: b2 in N and

       A9: b3 in N and

       A10: not b2 in M and

       A11: not a3 in N and

       A12: M _|_ N and

       A13: o <> a1 and

       A14: o <> a2 and o <> a3 and

       A15: o <> b1 and o <> b2 and

       A16: o <> b3 and

       A17: (a3,b2) // (a2,b1) and

       A18: (a3,b3) // (a1,b1);

      reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, b19 = b1, b29 = b2, b39 = b3 as Element of the AffinStruct of X;

      reconsider M9 = M, N9 = N as Subset of the AffinStruct of X;

      N is being_line by A12, ANALMETR: 44;

      then

       A19: N9 is being_line by ANALMETR: 43;

      M is being_line by A12, ANALMETR: 44;

      then

       A20: M9 is being_line by ANALMETR: 43;

       A21:

      now

        

         A22: not LIN (o9,b19,a19)

        proof

          (o9,a19) // (o9,a39) by A2, A3, A5, A20, AFF_1: 39, AFF_1: 41;

          then

           A23: LIN (o9,a19,a39) by AFF_1:def 1;

          assume LIN (o9,b19,a19);

          then a19 in N9 by A6, A7, A15, A19, AFF_1: 25;

          hence contradiction by A6, A11, A13, A19, A23, AFF_1: 25;

        end;

        

         A24: (b1,a2) // (a3,b2) by A17, ANALMETR: 59;

        (o9,a19) // (o9,a29) by A2, A3, A4, A20, AFF_1: 39, AFF_1: 41;

        then

         A25: LIN (o9,a19,a29) by AFF_1:def 1;

        assume

         A26: b2 = b3;

        then (b1,a1) // (a3,b2) by A18, ANALMETR: 59;

        then (b1,a1) // (b1,a2) by A5, A10, A24, ANALMETR: 60;

        then (b19,a19) // (b19,a29) by ANALMETR: 36;

        then a19 = a29 by A22, A25, AFF_1: 14;

        then (a19,b29) // (a29,b39) by A26, AFF_1: 2;

        hence thesis by ANALMETR: 36;

      end;

      

       A27: LIN (a,b,c) implies LIN (a,c,b) & LIN (b,a,c) & LIN (b,c,a) & LIN (c,a,b) & LIN (c,b,a)

      proof

        reconsider a9 = a, b9 = b, c9 = c as Element of the AffinStruct of X;

        assume LIN (a,b,c);

        then

         A28: LIN (a9,b9,c9) by ANALMETR: 40;

        then

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

        

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

        

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

        

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

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

        hence thesis by A29, A31, A30, A32, ANALMETR: 40;

      end;

       A33:

      now

        (o9,a39) // (o9,a19) by A2, A3, A5, A20, AFF_1: 39, AFF_1: 41;

        then LIN (o9,a39,a19) by AFF_1:def 1;

        then

         A34: LIN (o,a3,a1) by ANALMETR: 40;

        (a39,a19) // (a39,a29) by A3, A4, A5, A20, AFF_1: 39, AFF_1: 41;

        then LIN (a39,a19,a29) by AFF_1:def 1;

        then

         A35: LIN (a3,a1,a2) by ANALMETR: 40;

        (o9,b29) // (o9,b39) by A6, A8, A9, A19, AFF_1: 39, AFF_1: 41;

        then LIN (o9,b29,b39) by AFF_1:def 1;

        then

         A36: LIN (o,b2,b3) by ANALMETR: 40;

        assume that

         A37: a1 <> a3 and

         A38: b2 <> b3;

        

         A39: not LIN (a3,a1,b2) & not LIN (b2,a3,b3)

        proof

          assume LIN (a3,a1,b2) or LIN (b2,a3,b3);

          then LIN (a39,a19,b29) or LIN (b29,a39,b39) by ANALMETR: 40;

          then LIN (a39,a19,b29) or LIN (b29,b39,a39) by AFF_1: 6;

          hence contradiction by A3, A5, A8, A9, A10, A11, A20, A19, A37, A38, AFF_1: 25;

        end;

        (b29,b39) // (b29,b19) by A7, A8, A9, A19, AFF_1: 39, AFF_1: 41;

        then LIN (b29,b39,b19) by AFF_1:def 1;

        then

         A40: LIN (b2,b3,b1) by ANALMETR: 40;

         A41:

        now

          assume

           A42: b2 <> b1;

           not LIN (a2,a3,b3)

          proof

            

             A43: a3 <> a2

            proof

              assume a3 = a2;

              then LIN (a3,b2,b1) by A17, ANALMETR:def 10;

              then LIN (b2,b1,a3) by A27;

              then

               A44: (b2,b1) // (b2,a3) by ANALMETR:def 10;

               LIN (b2,b1,b3) by A27, A40;

              then (b2,b1) // (b2,b3) by ANALMETR:def 10;

              then (b2,a3) // (b2,b3) by A42, A44, ANALMETR: 60;

              hence contradiction by A39, ANALMETR:def 10;

            end;

             LIN (a3,a1,o) by A27, A34;

            then

             A45: (a3,a1) // (a3,o) by ANALMETR:def 10;

            

             A46: a3 <> a1

            proof

              assume a3 = a1;

              then LIN (a39,a19,b29) by AFF_1: 7;

              hence contradiction by A39, ANALMETR: 40;

            end;

            assume LIN (a2,a3,b3);

            then LIN (a3,a2,b3) by A27;

            then

             A47: (a3,a2) // (a3,b3) by ANALMETR:def 10;

             LIN (a3,a2,a1) by A27, A35;

            then (a3,a2) // (a3,a1) by ANALMETR:def 10;

            then (a3,a1) // (a3,b3) by A47, A43, ANALMETR: 60;

            then (a3,o) // (a3,b3) by A46, A45, ANALMETR: 60;

            then (a39,o9) // (a39,b39) by ANALMETR: 36;

            then

             A48: (a39,b39) // (a39,o9) by AFF_1: 4;

             LIN (b2,b3,o) by A27, A36;

            then

             A49: LIN (b29,b39,o9) by ANALMETR: 40;

             not LIN (b29,a39,b39) by A39, ANALMETR: 40;

            hence contradiction by A16, A48, A49, AFF_1: 14;

          end;

          then

          consider c1 such that

           A50: (c1,a2) _|_ (a3,b3) and

           A51: (c1,a3) _|_ (a2,b3) and

           A52: (c1,b3) _|_ (a2,a3) by A1, CONAFFM:def 3;

          reconsider c19 = c1 as Element of the AffinStruct of X;

           A53:

          now

            

             A54: a2 <> a3

            proof

              

               A55: not LIN (o9,a39,b19)

              proof

                assume LIN (o9,a39,b19);

                then LIN (o9,b19,a39) by AFF_1: 6;

                hence contradiction by A6, A7, A11, A15, A19, AFF_1: 25;

              end;

              assume a2 = a3;

              then (a39,b29) // (a39,b19) by A17, ANALMETR: 36;

              then

               A56: (a39,b19) // (a39,b29) by AFF_1: 4;

              (o9,b19) // (o9,b29) by A6, A7, A8, A19, AFF_1: 39, AFF_1: 41;

              then LIN (o9,b19,b29) by AFF_1:def 1;

              hence contradiction by A42, A55, A56, AFF_1: 14;

            end;

            (a2,a3) _|_ (b2,b3) by A4, A5, A8, A9, A12, ANALMETR: 56;

            then (b2,b3) // (c1,b3) by A52, A54, ANALMETR: 63;

            then (b3,b2) // (b3,c1) by ANALMETR: 59;

            then LIN (b3,b2,c1) by ANALMETR:def 10;

            then LIN (b39,b29,c19) by ANALMETR: 40;

            then

             A57: c1 in N by A8, A9, A19, A38, AFF_1: 25;

            

             A58: not LIN (o9,a29,c19)

            proof

              

               A59: o9 <> c19

              proof

                assume

                 A60: o9 = c19;

                (o,a2) _|_ (b3,b2) by A2, A4, A8, A9, A12, ANALMETR: 56;

                then (b3,b2) // (a3,b3) by A14, A50, A60, ANALMETR: 63;

                then (b3,b2) // (b3,a3) by ANALMETR: 59;

                then LIN (b3,b2,a3) by ANALMETR:def 10;

                then LIN (b39,b29,a39) by ANALMETR: 40;

                hence contradiction by A8, A9, A11, A19, A38, AFF_1: 25;

              end;

              (o9,a29) // (o9,a39) by A2, A4, A5, A20, AFF_1: 39, AFF_1: 41;

              then

               A61: LIN (o9,a29,a39) by AFF_1:def 1;

              assume LIN (o9,a29,c19);

              then LIN (o9,c19,a29) by AFF_1: 6;

              then a29 in N9 by A6, A19, A57, A59, AFF_1: 25;

              hence contradiction by A6, A11, A14, A19, A61, AFF_1: 25;

            end;

            

             A62: a1 <> b1

            proof

              (o9,b19) // (o9,b29) by A6, A7, A8, A19, AFF_1: 39, AFF_1: 41;

              then

               A63: LIN (o9,b19,b29) by AFF_1:def 1;

              assume a1 = b1;

              hence contradiction by A2, A3, A10, A13, A20, A63, AFF_1: 25;

            end;

            assume

             A64: a2 <> a1;

            

             A65: a1 <> b1

            proof

               LIN (a1,a2,a3) by A27, A35;

              then (a1,a2) // (a1,a3) by ANALMETR:def 10;

              then

               A66: (a2,a1) // (a3,a1) by ANALMETR: 59;

              assume a1 = b1;

              then (a3,a1) // (a3,b2) by A17, A64, A66, ANALMETR: 60;

              hence contradiction by A39, ANALMETR:def 10;

            end;

             not LIN (a2,a1,b1)

            proof

              assume LIN (a2,a1,b1);

              then LIN (b1,a1,a2) by A27;

              then (b1,a1) // (b1,a2) by ANALMETR:def 10;

              then (a1,b1) // (a2,b1) by ANALMETR: 59;

              then

               A67: (a2,b1) // (a3,b3) by A18, A65, ANALMETR: 60;

              a2 <> b1

              proof

                (o9,b19) // (o9,b29) by A6, A7, A8, A19, AFF_1: 39, AFF_1: 41;

                then

                 A68: LIN (o9,b19,b29) by AFF_1:def 1;

                assume a2 = b1;

                hence contradiction by A2, A4, A10, A14, A20, A68, AFF_1: 25;

              end;

              then (a3,b3) // (a3,b2) by A17, A67, ANALMETR: 60;

              then LIN (a3,b3,b2) by ANALMETR:def 10;

              hence contradiction by A27, A39;

            end;

            then

            consider c2 such that

             A69: (c2,a2) _|_ (a1,b1) and

             A70: (c2,a1) _|_ (a2,b1) and

             A71: (c2,b1) _|_ (a2,a1) by A1, CONAFFM:def 3;

            reconsider c29 = c2 as Element of the AffinStruct of X;

            (a1,b1) _|_ (c1,a2) by A9, A11, A18, A50, ANALMETR: 62;

            then (c2,a2) // (c1,a2) by A69, A62, ANALMETR: 63;

            then (a2,c1) // (a2,c2) by ANALMETR: 59;

            then

             A72: (a29,c19) // (a29,c29) by ANALMETR: 36;

            (a2,a1) _|_ (b1,b2) by A3, A4, A7, A8, A12, ANALMETR: 56;

            then (b1,b2) // (c2,b1) by A64, A71, ANALMETR: 63;

            then (b1,b2) // (b1,c2) by ANALMETR: 59;

            then LIN (b1,b2,c2) by ANALMETR:def 10;

            then LIN (b19,b29,c29) by ANALMETR: 40;

            then

             A73: c29 in N9 by A7, A8, A19, A42, AFF_1: 25;

            

             A74: not LIN (o9,a19,c29)

            proof

              

               A75: o9 <> c29

              proof

                

                 A76: a2 <> b1

                proof

                  (o9,b19) // (o9,b29) by A6, A7, A8, A19, AFF_1: 39, AFF_1: 41;

                  then

                   A77: LIN (o9,b19,b29) by AFF_1:def 1;

                  assume a2 = b1;

                  hence contradiction by A2, A4, A10, A14, A20, A77, AFF_1: 25;

                end;

                assume o9 = c29;

                then

                 A78: (o,a1) _|_ (a3,b2) by A17, A70, A76, ANALMETR: 62;

                (o,a1) _|_ (b3,b2) by A2, A3, A8, A9, A12, ANALMETR: 56;

                then (b3,b2) // (a3,b2) by A13, A78, ANALMETR: 63;

                then (b2,b3) // (b2,a3) by ANALMETR: 59;

                then LIN (b2,b3,a3) by ANALMETR:def 10;

                then LIN (b29,b39,a39) by ANALMETR: 40;

                hence contradiction by A8, A9, A11, A19, A38, AFF_1: 25;

              end;

              (o9,a19) // (o9,a39) by A2, A3, A5, A20, AFF_1: 39, AFF_1: 41;

              then

               A79: LIN (o9,a19,a39) by AFF_1:def 1;

              assume LIN (o9,a19,c29);

              then LIN (o9,c29,a19) by AFF_1: 6;

              then a19 in N9 by A6, A19, A73, A75, AFF_1: 25;

              hence contradiction by A6, A11, A13, A19, A79, AFF_1: 25;

            end;

             not LIN (a3,a1,b2)

            proof

              assume LIN (a3,a1,b2);

              then LIN (a39,a19,b29) by ANALMETR: 40;

              hence contradiction by A3, A5, A10, A20, A37, AFF_1: 25;

            end;

            then

            consider c3 such that

             A80: (c3,a3) _|_ (a1,b2) and

             A81: (c3,a1) _|_ (a3,b2) and

             A82: (c3,b2) _|_ (a3,a1) by A1, CONAFFM:def 3;

            reconsider c39 = c3 as Element of the AffinStruct of X;

            a2 <> b1

            proof

              (o9,b19) // (o9,b29) by A6, A7, A8, A19, AFF_1: 39, AFF_1: 41;

              then

               A83: LIN (o9,b19,b29) by AFF_1:def 1;

              assume a2 = b1;

              hence contradiction by A2, A4, A10, A14, A20, A83, AFF_1: 25;

            end;

            then (a3,b2) _|_ (c2,a1) by A17, A70, ANALMETR: 62;

            then (c2,a1) // (c3,a1) by A5, A10, A81, ANALMETR: 63;

            then (a1,c2) // (a1,c3) by ANALMETR: 59;

            then

             A84: (a19,c29) // (a19,c39) by ANALMETR: 36;

            (a2,a1) _|_ (b2,b1) by A3, A4, A7, A8, A12, ANALMETR: 56;

            then (b2,b1) // (c2,b1) by A64, A71, ANALMETR: 63;

            then (b1,b2) // (b1,c2) by ANALMETR: 59;

            then LIN (b1,b2,c2) by ANALMETR:def 10;

            then LIN (b19,b29,c29) by ANALMETR: 40;

            then c2 in N by A7, A8, A19, A42, AFF_1: 25;

            then (o9,c19) // (o9,c29) by A6, A19, A57, AFF_1: 39, AFF_1: 41;

            then LIN (o9,c19,c29) by AFF_1:def 1;

            then

             A85: c1 = c2 by A58, A72, AFF_1: 14;

            

             A86: c1 <> a3

            proof

              

               A87: a2 <> a3

              proof

                

                 A88: not LIN (o9,a39,b19)

                proof

                  assume LIN (o9,a39,b19);

                  then LIN (o9,b19,a39) by AFF_1: 6;

                  hence contradiction by A6, A7, A11, A15, A19, AFF_1: 25;

                end;

                assume a2 = a3;

                then (a39,b29) // (a39,b19) by A17, ANALMETR: 36;

                then

                 A89: (a39,b19) // (a39,b29) by AFF_1: 4;

                (o9,b19) // (o9,b29) by A6, A7, A8, A19, AFF_1: 39, AFF_1: 41;

                then LIN (o9,b19,b29) by AFF_1:def 1;

                hence contradiction by A42, A88, A89, AFF_1: 14;

              end;

              assume

               A90: c1 = a3;

              (a2,a3) _|_ (b2,b3) by A4, A5, A8, A9, A12, ANALMETR: 56;

              then (a3,b3) // (b2,b3) by A52, A90, A87, ANALMETR: 63;

              then (b3,b2) // (b3,a3) by ANALMETR: 59;

              then LIN (b3,b2,a3) by ANALMETR:def 10;

              then LIN (b39,b29,a39) by ANALMETR: 40;

              hence contradiction by A8, A9, A11, A19, A38, AFF_1: 25;

            end;

            (a3,a1) _|_ (b2,b3) by A3, A5, A8, A9, A12, ANALMETR: 56;

            then (c3,b2) // (b2,b3) by A37, A82, ANALMETR: 63;

            then (b2,b3) // (b2,c3) by ANALMETR: 59;

            then LIN (b2,b3,c3) by ANALMETR:def 10;

            then LIN (b29,b39,c39) by ANALMETR: 40;

            then c39 in N9 by A8, A9, A19, A38, AFF_1: 25;

            then (o9,c29) // (o9,c39) by A6, A19, A73, AFF_1: 39, AFF_1: 41;

            then LIN (o9,c29,c39) by AFF_1:def 1;

            then c2 = c3 by A74, A84, AFF_1: 14;

            hence thesis by A51, A85, A80, A86, ANALMETR: 63;

          end;

          now

            (o9,b29) // (o9,b39) by A6, A8, A9, A19, AFF_1: 39, AFF_1: 41;

            then

             A91: LIN (o9,b29,b39) by AFF_1:def 1;

            assume

             A92: a2 = a1;

            a1 <> b1

            proof

              (o9,b19) // (o9,b29) by A6, A7, A8, A19, AFF_1: 39, AFF_1: 41;

              then

               A93: LIN (o9,b19,b29) by AFF_1:def 1;

              assume a1 = b1;

              hence contradiction by A2, A3, A10, A13, A20, A93, AFF_1: 25;

            end;

            then (a3,b2) // (a3,b3) by A17, A18, A92, ANALMETR: 60;

            then (a39,b29) // (a39,b39) by ANALMETR: 36;

            then b29 = b39 by A2, A5, A6, A10, A11, A20, A91, AFF_1: 14, AFF_1: 25;

            then (a19,b29) // (a29,b39) by A92, AFF_1: 2;

            hence thesis by ANALMETR: 36;

          end;

          hence thesis by A53;

        end;

        now

          

           A94: not LIN (o9,b29,a39)

          proof

            assume LIN (o9,b29,a39);

            then LIN (o,b2,a3) by ANALMETR: 40;

            then LIN (b2,o,a3) by A27;

            then

             A95: (b2,o) // (b2,a3) by ANALMETR:def 10;

             LIN (b2,o,b3) by A27, A36;

            then (b2,o) // (b2,b3) by ANALMETR:def 10;

            then (b2,a3) // (b2,b3) by A2, A10, A95, ANALMETR: 60;

            hence contradiction by A39, ANALMETR:def 10;

          end;

           LIN (a3,a1,o) by A27, A34;

          then

           A96: (a3,a1) // (a3,o) by ANALMETR:def 10;

          

           A97: a3 <> a1

          proof

            assume a3 = a1;

            then LIN (a39,a19,b29) by AFF_1: 7;

            hence contradiction by A39, ANALMETR: 40;

          end;

          (a3,a1) // (a3,a2) by A35, ANALMETR:def 10;

          then (a3,o) // (a3,a2) by A96, A97, ANALMETR: 60;

          then LIN (a3,o,a2) by ANALMETR:def 10;

          then LIN (o,a3,a2) by A27;

          then

           A98: LIN (o9,a39,a29) by ANALMETR: 40;

          assume

           A99: b2 = b1;

          then (b2,a3) // (b2,a2) by A17, ANALMETR: 59;

          then (b29,a39) // (b29,a29) by ANALMETR: 36;

          then a39 = a29 by A98, A94, AFF_1: 14;

          hence thesis by A18, A99, ANALMETR: 59;

        end;

        hence thesis by A41;

      end;

      now

        

         A100: not LIN (o9,a19,b19)

        proof

          (o9,b19) // (o9,b29) by A6, A7, A8, A19, AFF_1: 39, AFF_1: 41;

          then

           A101: LIN (o9,b19,b29) by AFF_1:def 1;

          assume LIN (o9,a19,b19);

          then b19 in M9 by A2, A3, A13, A20, AFF_1: 25;

          hence contradiction by A2, A10, A15, A20, A101, AFF_1: 25;

        end;

        (o9,b19) // (o9,b39) by A6, A7, A9, A19, AFF_1: 39, AFF_1: 41;

        then

         A102: LIN (o9,b19,b39) by AFF_1:def 1;

        assume

         A103: a1 = a3;

        then (a1,b1) // (a1,b3) by A18, ANALMETR: 59;

        then (a19,b19) // (a19,b39) by ANALMETR: 36;

        hence thesis by A17, A103, A100, A102, AFF_1: 14;

      end;

      hence thesis by A21, A33;

    end;