conaffm.miz



    begin

    reserve X for OrtAfPl;

    reserve o,a,a1,a2,b,b1,b2,c,c1,c2,d,e1,e2 for Element of X;

    reserve b29,c29,d19 for Element of the AffinStruct of X;

    definition

      let X;

      :: CONAFFM:def1

      attr X is satisfying_DES 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 (a,a1,c) & LIN (o,a,a1) & LIN (o,b,b1) & LIN (o,c,c1) & (a,b) // (a1,b1) & (a,c) // (a1,c1) holds (b,c) // (b1,c1);

      :: CONAFFM:def2

      attr X is satisfying_AH means for o, a, a1, b, b1, c, c1 st (o,a) _|_ (o,a1) & (o,b) _|_ (o,b1) & (o,c) _|_ (o,c1) & (a,b) _|_ (a1,b1) & (o,a) // (b,c) & (a,c) _|_ (a1,c1) & not (o,c) // (o,a) & not (o,a) // (o,b) holds (b,c) _|_ (b1,c1);

      :: CONAFFM:def3

      attr X is satisfying_3H means for a, b, c st not LIN (a,b,c) holds ex d st (d,a) _|_ (b,c) & (d,b) _|_ (a,c) & (d,c) _|_ (a,b);

      :: CONAFFM:def4

      attr X is satisfying_ODES means for o, a, a1, b, b1, c, c1 st (o,a) _|_ (o,a1) & (o,b) _|_ (o,b1) & (o,c) _|_ (o,c1) & (a,b) _|_ (a1,b1) & (a,c) _|_ (a1,c1) & not (o,c) // (o,a) & not (o,a) // (o,b) holds (b,c) _|_ (b1,c1);

      :: CONAFFM:def5

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

      :: CONAFFM:def6

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

      :: CONAFFM:def7

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

    end

    theorem :: CONAFFM:1

    X is satisfying_ODES implies X is satisfying_DES

    proof

      assume

       A1: X is satisfying_ODES;

      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 o <> c1 and

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

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

       A9: LIN (o,a,a1) and

       A10: LIN (o,b,b1) and

       A11: LIN (o,c,c1) and

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

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

      consider a2 such that

       A14: (o,a) _|_ (o,a2) and

       A15: o <> a2 by ANALMETR:def 9;

      consider e1 such that

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

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

      consider e2 such that

       A18: (a,b) _|_ (a2,e2) and

       A19: a2 <> e2 by ANALMETR:def 9;

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

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

      proof

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

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

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

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

        then

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

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

        then

         A21: LIN (b9,a9,o9) by AFF_1:def 1;

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

        then

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

        

         A23: b9 <> a9

        proof

          assume b9 = a9;

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

          hence contradiction by A7, ANALMETR: 40;

        end;

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

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

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

        then LIN (b9,a9,b19) by A21, A23, AFF_1: 9;

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

        hence contradiction by A7, ANALMETR: 40;

      end;

      then

      consider b29 such that

       A24: LIN (o9,e19,b29) and

       A25: LIN (a29,e29,b29) by AFF_1: 60;

      reconsider b2 = b29 as Element of X;

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

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

      then

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

       LIN (a2,e2,b2) by A25, ANALMETR: 40;

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

      then

       A27: (a,b) _|_ (a2,b2) by A18, A19, ANALMETR: 62;

      consider e1 such that

       A28: (o,c) _|_ (o,e1) and

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

      consider e2 such that

       A30: (a,c) _|_ (a2,e2) and

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

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

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

      proof

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

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

        then (o,c) _|_ (a2,e2) by A28, A29, ANALMETR: 62;

        then (o,c) // (a,c) by A30, A31, ANALMETR: 63;

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

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

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

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

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

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

        then

         A32: (o,a) // (a,c) by ANALMETR: 59;

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

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

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

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

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

        then (a,a1) // (a,c) by A2, A32, ANALMETR: 60;

        hence contradiction by A8, ANALMETR:def 10;

      end;

      then

      consider c29 such that

       A33: LIN (o9,e19,c29) and

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

      reconsider c2 = c29 as Element of X;

       LIN (o,e1,c2) by A33, ANALMETR: 40;

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

      then

       A35: (o,c) _|_ (o,c2) by A28, A29, ANALMETR: 62;

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

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

      then

       A36: (a,c) _|_ (a2,c2) by A30, A31, ANALMETR: 62;

      

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

      proof

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

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

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

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

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

        then

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

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

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

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

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

        then (a,a1) // (a,c) by A2, A38, ANALMETR: 60;

        hence contradiction by A8, ANALMETR:def 10;

      end;

       not (o,a) // (o,b)

      proof

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

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

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

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

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

        then

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

         LIN (o9,b9,b19) by A10, 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,a) by A4, A39, ANALMETR: 60;

        hence contradiction by A7, ANALMETR:def 10;

      end;

      then

       A40: (b,c) _|_ (b2,c2) by A1, A14, A26, A27, A35, A36, A37;

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

      then

       A41: (o,a1) _|_ (o,a2) by A2, A14, ANALMETR: 62;

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

      then

       A42: (o,b1) _|_ (o,b2) by A4, A26, ANALMETR: 62;

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

      then

       A43: (o,c1) _|_ (o,c2) by A6, A35, ANALMETR: 62;

      a <> b

      proof

        assume a = b;

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

        hence contradiction by A7, ANALMETR: 40;

      end;

      then

       A44: (a1,b1) _|_ (a2,b2) by A12, A27, ANALMETR: 62;

      a <> c

      proof

        assume a = c;

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

        hence contradiction by A8, ANALMETR: 40;

      end;

      then

       A45: (a1,c1) _|_ (a2,c2) by A13, A36, ANALMETR: 62;

      

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

      proof

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

        then LIN (o,c1,a1) by ANALMETR:def 10;

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

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

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

        then

         A47: (a1,o) // (a1,c1) by ANALMETR:def 10;

        

         A48: a1 <> c1

        proof

          assume a1 = c1;

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

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

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

          then

           A49: (a1,c) // (a1,o) by ANALMETR:def 10;

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

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

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

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

          then (a1,c) // (a1,a) by A3, A49, ANALMETR: 60;

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

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

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

          hence contradiction by A8, ANALMETR: 40;

        end;

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

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

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

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

        then (a1,c1) // (a1,a) by A3, A47, ANALMETR: 60;

        then (a1,a) // (a,c) by A13, A48, ANALMETR: 60;

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

        hence contradiction by A8, ANALMETR:def 10;

      end;

       not (o,a1) // (o,b1)

      proof

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

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

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

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

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

        then

         A50: (b1,a1) // (b1,o) by ANALMETR:def 10;

        

         A51: a1 <> b1

        proof

          assume a1 = b1;

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

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

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

          then

           A52: (b1,o) // (b1,a) by ANALMETR:def 10;

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

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

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

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

          then (b1,a) // (b1,b) by A5, A52, ANALMETR: 60;

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

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

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

          hence contradiction by A7, ANALMETR: 40;

        end;

        

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

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

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

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

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

        then (b1,a1) // (b1,b) by A5, A50, ANALMETR: 60;

        then (b1,b) // (a,b) by A51, A53, ANALMETR: 60;

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

        hence contradiction by A7, ANALMETR:def 10;

      end;

      then

       A54: (b1,c1) _|_ (b2,c2) by A1, A41, A42, A43, A44, A45, A46;

       A55:

      now

        assume

         A56: not LIN (o,b,c);

        b2 <> c2

        proof

          assume

           A57: b2 = c2;

          o <> b2

          proof

            assume

             A58: o = b2;

            (a2,o) _|_ (a,o) by A14, ANALMETR: 61;

            then (a,o) // (a,b) by A15, A27, A58, ANALMETR: 63;

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

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

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

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

            then

             A59: (b,o) // (b,a) by ANALMETR:def 10;

             LIN (o9,b9,b19) by A10, 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,a) by A4, A59, ANALMETR: 60;

            hence contradiction by A7, ANALMETR:def 10;

          end;

          then (o,b) // (o,c) by A26, A35, A57, ANALMETR: 63;

          hence contradiction by A56, ANALMETR:def 10;

        end;

        hence thesis by A40, A54, ANALMETR: 63;

      end;

      now

        assume

         A60: LIN (o,b,c);

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

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

        then

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

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

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

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

        then (b9,c9) // (b9,b19) by A4, A61, AFF_1: 5;

        then

         A62: LIN (b9,c9,b19) by AFF_1:def 1;

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

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

        then

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

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

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

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

        then (c9,b9) // (c9,c19) by A6, A63, AFF_1: 5;

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

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

        then (b9,c9) // (b19,c19) by A62, AFF_1: 10;

        hence thesis by ANALMETR: 36;

      end;

      hence thesis by A55;

    end;

    theorem :: CONAFFM:2

    X is satisfying_ODES implies X is satisfying_AH;

    theorem :: CONAFFM:3

    

     Th3: X is satisfying_LIN implies X is satisfying_LIN1

    proof

      assume

       A1: X is satisfying_LIN;

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

      assume that

       A2: o <> a and

       A3: o <> a1 and

       A4: o <> b and o <> b1 and

       A5: o <> c and

       A6: o <> c1 and

       A7: a <> b and

       A8: (o,c) _|_ (o,c1) and

       A9: (o,a) _|_ (o,a1) and (o,b) _|_ (o,b1) and

       A10: not LIN (o,c,a) and

       A11: LIN (o,a,b) and

       A12: LIN (o,a1,b1) and

       A13: (a,c) _|_ (a1,c1) and

       A14: (a,a1) // (b,b1);

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

      now

        ex b2 st LIN (o,a1,b2) & (c1,b2) _|_ (b,c) & c1 <> b2

        proof

          consider y be Element of X such that

           A15: (o,a1) // (o,y) and

           A16: o <> y by ANALMETR: 39;

          consider x be Element of X such that

           A17: (b,c) _|_ (c1,x) and

           A18: c1 <> x by ANALMETR: 39;

          

           A19: not (o,y) // (c1,x)

          proof

            assume

             A20: (o,y) // (c1,x);

            reconsider y9 = y, x9 = x as Element of the AffinStruct of X;

            

             A21: (o9,y9) // (c19,x9) by A20, ANALMETR: 36;

            (o9,a19) // (o9,y9) by A15, ANALMETR: 36;

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

            then (c19,x9) // (o9,a19) by A16, A21, DIRAF: 40;

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

            then (o,a1) _|_ (b,c) by A17, A18, ANALMETR: 62;

            then

             A22: (o,a) // (b,c) by A3, A9, ANALMETR: 63;

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

            then (b,c) // (o,b) by A2, A22, ANALMETR: 60;

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

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

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

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

            then

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

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

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

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

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

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

            hence contradiction by A10, ANALMETR: 40;

          end;

          reconsider y9 = y, x9 = x as Element of the AffinStruct of X;

           not (o9,y9) // (c19,x9) by A19, ANALMETR: 36;

          then

          consider b29 be Element of the AffinStruct of X such that

           A24: LIN (o9,y9,b29) and

           A25: LIN (c19,x9,b29) by AFF_1: 60;

          reconsider b2 = b29 as Element of X;

           LIN (c1,x,b2) by A25, ANALMETR: 40;

          then (c1,x) // (c1,b2) by ANALMETR:def 10;

          then

           A26: (c1,b2) _|_ (b,c) by A17, A18, ANALMETR: 62;

          (o9,a19) // (o9,y9) by A15, ANALMETR: 36;

          then

           A27: (o9,y9) // (o9,a19) by AFF_1: 4;

          (o9,y9) // (o9,b29) by A24, AFF_1:def 1;

          then (o9,a19) // (o9,b29) by A16, A27, DIRAF: 40;

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

          then

           A28: LIN (o,a1,b2) by ANALMETR: 40;

          c1 <> b2

          proof

            assume c1 = b2;

            then (o,a1) // (o,c1) by A28, ANALMETR:def 10;

            then (o,c1) _|_ (o,a) by A3, A9, ANALMETR: 62;

            then (o,c) // (o,a) by A6, A8, ANALMETR: 63;

            hence contradiction by A10, ANALMETR:def 10;

          end;

          hence thesis by A26, A28;

        end;

        then

        consider b2 such that

         A29: LIN (o,a1,b2) and

         A30: (c1,b2) _|_ (b,c) and c1 <> b2;

        reconsider b29 = b2 as Element of the AffinStruct of X;

        (o,a1) // (o,b2) by A29, ANALMETR:def 10;

        then

         A31: (o,a) _|_ (o,b2) by A3, A9, ANALMETR: 62;

        

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

        

         A33: o <> b2

        proof

          assume o = b2;

          then (o,c1) _|_ (b,c) by A30, ANALMETR: 61;

          then (o,c) // (b,c) by A6, A8, ANALMETR: 63;

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

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

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

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

          then

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

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

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

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

          then (o9,c9) // (o9,a9) by A4, A34, DIRAF: 40;

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

          hence contradiction by A10, ANALMETR: 40;

        end;

        

         A35: (o,b) _|_ (o,b2) by A2, A31, A32, ANALMETR: 62;

        (b,c) _|_ (b2,c1) by A30, ANALMETR: 61;

        then

         A36: (a,a1) // (b,b2) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A13, A29, A33, A35;

         not LIN (o,a,a1)

        proof

          assume LIN (o,a,a1);

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

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

          hence contradiction by A3, ANALMETR: 39;

        end;

        then

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

        

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

        

         A39: LIN (o9,a19,b19) by A12, ANALMETR: 40;

        

         A40: LIN (o9,a19,b29) by A29, ANALMETR: 40;

        

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

        (a9,a19) // (b9,b29) by A36, ANALMETR: 36;

        then b1 = b2 by A37, A38, A39, A40, A41, AFF_1: 56;

        hence thesis by A30, ANALMETR: 61;

      end;

      hence thesis;

    end;

    theorem :: CONAFFM:4

    X is satisfying_LIN1 implies X is satisfying_LIN2

    proof

      assume

       A1: X is satisfying_LIN1;

      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 o <> c1 and

       A7: a <> b and

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

       A9: (o,a) _|_ (o,a1) and

       A10: (o,b) _|_ (o,b1) and

       A11: not LIN (o,c,a) and

       A12: LIN (o,a,b) and

       A13: LIN (o,a1,b1) and

       A14: (a,c) _|_ (a1,c1) and

       A15: (b,c) _|_ (b1,c1);

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

      ex c2 st LIN (a1,c1,c2) & (o,c) _|_ (o,c2) & o <> c2

      proof

        consider e1 such that

         A16: (a1,c1) // (a1,e1) and

         A17: a1 <> e1 by ANALMETR: 39;

        consider e2 such that

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

         A19: o <> e2 by ANALMETR: 39;

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

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

        proof

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

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

          then (a1,c1) // (o,e2) by A16, A17, ANALMETR: 60;

          then

           A20: (a1,c1) _|_ (o,c) by A18, A19, ANALMETR: 62;

          a1 <> c1

          proof

            assume

             A21: a1 = c1;

            

             A22: b1 <> a1

            proof

              assume b1 = a1;

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

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

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

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

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

              then

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

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

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

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

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

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

              then (a,a1) // (o,a) by A7, A23, ANALMETR: 60;

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

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

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

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

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

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

              then (o,a) _|_ (o,a) by A3, A9, ANALMETR: 62;

              hence contradiction by A2, ANALMETR: 39;

            end;

            

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

            

             A25: LIN (o9,a19,b19) by A13, ANALMETR: 40;

            

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

            

             A27: LIN (b19,o9,a19) by A25, AFF_1: 6;

            

             A28: LIN (b,o,a) by A26, ANALMETR: 40;

            

             A29: LIN (b1,o,a1) by A27, ANALMETR: 40;

            

             A30: (b,o) // (b,a) by A28, ANALMETR:def 10;

            

             A31: (b1,o) // (b1,a1) by A29, ANALMETR:def 10;

            (b,o) _|_ (b1,o) by A10, ANALMETR: 61;

            then (b,a) _|_ (b1,o) by A4, A30, ANALMETR: 62;

            then (b1,a1) _|_ (b,a) by A5, A31, ANALMETR: 62;

            then (b,c) // (b,a) by A15, A21, A22, ANALMETR: 63;

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

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

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

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

            then

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

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

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

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

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

            then (a,c) // (a,o) by A7, A32, ANALMETR: 60;

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

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

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

            hence contradiction by A11, ANALMETR: 40;

          end;

          then (a,c) // (o,c) by A14, A20, ANALMETR: 63;

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

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

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

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

          hence contradiction by A11, ANALMETR: 40;

        end;

        then

        consider c29 such that

         A33: LIN (a19,e19,c29) and

         A34: LIN (o9,e29,c29) by AFF_1: 60;

        reconsider c2 = c29 as Element of X;

        take c2;

        (a19,e19) // (a19,c29) by A33, AFF_1:def 1;

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

        then

         A35: (a1,c1) // (a1,c2) by A16, A17, ANALMETR: 60;

         LIN (o,e2,c2) by A34, ANALMETR: 40;

        then

         A36: (o,e2) // (o,c2) by ANALMETR:def 10;

        o <> c2

        proof

          assume o = c2;

          then (a1,c1) // (o,a1) by A35, ANALMETR: 59;

          then

           A37: (o,a) _|_ (a1,c1) by A3, A9, ANALMETR: 62;

          a1 <> c1

          proof

            assume

             A38: a1 = c1;

            

             A39: a1 <> b1

            proof

              assume a1 = b1;

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

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

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

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

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

              then

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

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

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

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

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

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

              then (a,a1) // (o,a) by A7, A40, ANALMETR: 60;

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

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

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

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

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

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

              then (o,a) _|_ (o,a) by A3, A9, ANALMETR: 62;

              hence contradiction by A2, ANALMETR: 39;

            end;

             LIN (o9,a19,b19) by A13, ANALMETR: 40;

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

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

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

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

            then (b,c) _|_ (o,b1) by A15, A38, A39, ANALMETR: 62;

            then

             A41: (b,c) // (o,b) by A5, A10, ANALMETR: 63;

            

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

            then

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

            

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

            

             A45: LIN (b,a,o) by A43, ANALMETR: 40;

            

             A46: LIN (a,b,o) by A44, ANALMETR: 40;

            

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

            

             A48: (a,b) // (a,o) by A46, ANALMETR:def 10;

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

            then (b,a) // (b,c) by A4, A41, 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;

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

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

            then (a,o) // (a,c) by A7, A48, ANALMETR: 60;

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

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

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

            hence contradiction by A11, ANALMETR: 40;

          end;

          then (o,a) // (a,c) by A14, A37, ANALMETR: 63;

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

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

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

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

          hence contradiction by A11, ANALMETR: 40;

        end;

        hence thesis by A18, A19, A35, A36, ANALMETR: 62, ANALMETR:def 10;

      end;

      then

      consider c2 such that

       A49: LIN (a1,c1,c2) and

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

       A51: o <> c2;

      reconsider c29 = c2 as Element of the AffinStruct of X;

      

       A52: b <> c & a1 <> b1 & a1 <> c1

      proof

        assume

         A53: b = c or a1 = b1 or a1 = c1;

         A54:

        now

          assume b = c;

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

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

          hence contradiction by A11, ANALMETR: 40;

        end;

         A55:

        now

          assume a1 = b1;

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

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

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

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

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

          then

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

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

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

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

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

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

          then (a,a1) // (o,a) by A7, A56, ANALMETR: 60;

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

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

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

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

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

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

          then (o,a) _|_ (o,a) by A3, A9, ANALMETR: 62;

          hence contradiction by A2, ANALMETR: 39;

        end;

        now

          assume

           A57: a1 = c1;

           LIN (o9,a19,b19) by A13, ANALMETR: 40;

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

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

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

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

          then (b,c) _|_ (o,b1) by A15, A55, A57, ANALMETR: 62;

          then

           A58: (b,c) // (o,b) by A5, A10, ANALMETR: 63;

          

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

          then

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

          

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

          

           A62: LIN (b,a,o) by A60, ANALMETR: 40;

          

           A63: LIN (a,b,o) by A61, ANALMETR: 40;

          

           A64: (b,a) // (b,o) by A62, ANALMETR:def 10;

          

           A65: (a,b) // (a,o) by A63, ANALMETR:def 10;

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

          then (b,a) // (b,c) by A4, A58, 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;

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

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

          then (a,o) // (a,c) by A7, A65, ANALMETR: 60;

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

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

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

          hence contradiction by A11, ANALMETR: 40;

        end;

        hence contradiction by A53, A54, A55;

      end;

      (a1,c1) // (a1,c2) by A49, ANALMETR:def 10;

      then (a,c) _|_ (a1,c2) by A14, A52, ANALMETR: 62;

      then (b,c) _|_ (b1,c2) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A50, A51;

      then (b1,c1) // (b1,c2) by A15, A52, ANALMETR: 63;

      then

       A66: LIN (b1,c1,c2) by ANALMETR:def 10;

       not LIN (b1,a1,c1)

      proof

        assume LIN (b1,a1,c1);

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

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

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

        then

         A67: (a1,b1) // (a1,c1) by ANALMETR: 36;

         LIN (o9,a19,b19) by A13, ANALMETR: 40;

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

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

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

        then (a1,c1) // (a1,o) by A52, A67, ANALMETR: 60;

        then (a,c) _|_ (a1,o) by A14, A52, ANALMETR: 62;

        then

         A68: (o,a1) _|_ (a,c) by ANALMETR: 61;

        (o,a1) _|_ (a,o) by A9, ANALMETR: 61;

        then (a,o) // (a,c) by A3, A68, ANALMETR: 63;

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

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

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

        hence contradiction by A11, ANALMETR: 40;

      end;

      then

       A69: not LIN (b19,a19,c19) by ANALMETR: 40;

      

       A70: LIN (b19,c19,c29) by A66, ANALMETR: 40;

      (a1,c1) // (a1,c2) by A49, ANALMETR:def 10;

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

      hence thesis by A50, A69, A70, AFF_1: 14;

    end;

    theorem :: CONAFFM:5

    X is satisfying_LIN implies X is satisfying_ODES

    proof

      assume

       A1: X is satisfying_LIN;

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

      assume that

       A2: (o,a) _|_ (o,a1) and

       A3: (o,b) _|_ (o,b1) and

       A4: (o,c) _|_ (o,c1) and

       A5: (a,b) _|_ (a1,b1) and

       A6: (a,c) _|_ (a1,c1) and

       A7: not (o,c) // (o,a) and

       A8: not (o,a) // (o,b);

      

       A9: X is satisfying_LIN1 by A1, Th3;

      now

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

        assume

         A10: X is satisfying_LIN;

        assume that

         A11: (o,a) _|_ (o,a1) and

         A12: (o,b) _|_ (o,b1) and

         A13: (o,c) _|_ (o,c1) and

         A14: (a,b) _|_ (a1,b1) and

         A15: (a,c) _|_ (a1,c1) and

         A16: not (o,c) // (o,a) and

         A17: not (o,a) // (o,b);

        assume

         A18: not (o,b) // (a,c);

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

         A19:

        now

          assume

           A20: o = a1;

          then

           A21: (a1,b1) _|_ (b,a1) by A12, ANALMETR: 61;

          

           A22: (a1,b1) _|_ (b,a) by A14, ANALMETR: 61;

           not (b,a1) // (b,a)

          proof

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

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

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

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

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

            hence contradiction by A17, ANALMETR:def 10;

          end;

          then

           A23: a1 = b1 by A21, A22, ANALMETR: 63;

          

           A24: (a1,c1) _|_ (c,a1) by A13, A20, ANALMETR: 61;

          (a1,c1) _|_ (c,a) by A15, ANALMETR: 61;

          then

           A25: (c,a1) // (c,a) or a1 = c1 by A24, ANALMETR: 63;

           not (c,a1) // (c,a)

          proof

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

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

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

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

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

            hence contradiction by A16, ANALMETR:def 10;

          end;

          hence (b,c) _|_ (b1,c1) by A23, A25, ANALMETR: 39;

        end;

         A26:

        now

          assume that

           A27: LIN (o,b,c) and

           A28: o <> a1;

          

           A29: o <> b by A17, ANALMETR: 39;

          

           A30: o <> c

          proof

            assume o = c;

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

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

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

            hence contradiction by A16, ANALMETR: 36;

          end;

          

           A31: o <> b1

          proof

            assume

             A32: o = b1;

            (a1,o) _|_ (a,o) by A11, ANALMETR: 61;

            then (a,o) // (a,b) by A14, A28, A32, ANALMETR: 63;

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

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

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

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

            hence contradiction by A17, ANALMETR:def 10;

          end;

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

          then (o,c) _|_ (o,b1) by A12, A29, ANALMETR: 62;

          then (o,b1) // (o,c1) by A13, A30, ANALMETR: 63;

          then LIN (o,b1,c1) by ANALMETR:def 10;

          then LIN (o9,b19,c19) by ANALMETR: 40;

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

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

          then

           A33: (b1,o) // (b1,c1) by ANALMETR:def 10;

          (b1,o) _|_ (b,o) by A12, ANALMETR: 61;

          then

           A34: (b,o) _|_ (b1,c1) by A31, A33, ANALMETR: 62;

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

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

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

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

          hence (b,c) _|_ (b1,c1) by A29, A34, ANALMETR: 62;

        end;

         A35:

        now

          assume that

           A36: LIN (a,b,c) and not LIN (o,b,c) and

           A37: o <> a1;

          

           A38: a <> c

          proof

            assume a = c;

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

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

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

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

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

            hence contradiction by A16, ANALMETR:def 10;

          end;

          

           A39: a <> b

          proof

            assume a = b;

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

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

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

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

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

            hence contradiction by A17, ANALMETR:def 10;

          end;

          

           A40: a1 <> b1 by A11, A12, A17, A37, ANALMETR: 63;

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

          then (a,c) _|_ (a1,b1) by A14, A39, ANALMETR: 62;

          then (a1,b1) // (a1,c1) by A15, A38, ANALMETR: 63;

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

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

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

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

          then

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

          (b1,a1) _|_ (b,a) by A14, ANALMETR: 61;

          then

           A42: (b,a) _|_ (b1,c1) by A40, A41, ANALMETR: 62;

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

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

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

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

          hence (b,c) _|_ (b1,c1) by A39, A42, ANALMETR: 62;

        end;

        now

          assume that

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

           A44: not LIN (o,b,c) and

           A45: o <> a1;

          

           A46: o <> c

          proof

            assume o = c;

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

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

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

            hence contradiction by A16, ANALMETR: 36;

          end;

          

           A47: o <> b1

          proof

            assume

             A48: o = b1;

            (a1,o) _|_ (a,o) by A11, ANALMETR: 61;

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

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

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

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

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

            hence contradiction by A17, ANALMETR:def 10;

          end;

          

           A49: o <> c1

          proof

            assume

             A50: o = c1;

            (a1,o) _|_ (a,o) by A11, ANALMETR: 61;

            then (a,o) // (a,c) by A15, A45, A50, ANALMETR: 63;

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

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

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

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

            hence contradiction by A16, ANALMETR:def 10;

          end;

          

           A51: o <> a by A16, ANALMETR: 39;

          

           A52: o <> b by A17, ANALMETR: 39;

          

           A53: a <> c by A13, A16, A49, ANALMETR: 63;

          

           A54: a1 <> c1 by A11, A13, A16, A49, ANALMETR: 63;

          ex e be Element of X st LIN (o,e,b) & LIN (a,c,e) & e <> c & e <> b

          proof

            consider p be Element of X such that

             A55: (o,b) // (o,p) and

             A56: o <> p by ANALMETR: 39;

            reconsider p9 = p as Element of the AffinStruct of X;

            consider p1 be Element of X such that

             A57: (a,c) // (a,p1) and

             A58: a <> p1 by ANALMETR: 39;

            reconsider p19 = p1 as Element of the AffinStruct of X;

             not (o,p) // (a,p1)

            proof

              assume (o,p) // (a,p1);

              then (a,p1) // (o,b) by A55, A56, ANALMETR: 60;

              hence contradiction by A18, A57, A58, ANALMETR: 60;

            end;

            then not (o9,p9) // (a9,p19) by ANALMETR: 36;

            then

            consider e9 be Element of the AffinStruct of X such that

             A59: LIN (o9,p9,e9) and

             A60: LIN (a9,p19,e9) by AFF_1: 60;

            reconsider e = e9 as Element of X;

             LIN (o,p,e) by A59, ANALMETR: 40;

            then (o,p) // (o,e) by ANALMETR:def 10;

            then (o,e) // (o,b) by A55, A56, ANALMETR: 60;

            then

             A61: LIN (o,e,b) by ANALMETR:def 10;

             LIN (a,p1,e) by A60, ANALMETR: 40;

            then (a,p1) // (a,e) by ANALMETR:def 10;

            then (a,c) // (a,e) by A57, A58, ANALMETR: 60;

            then

             A62: LIN (a,c,e) by ANALMETR:def 10;

            

             A63: c <> e

            proof

              assume c = e;

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

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

              hence contradiction by A44, ANALMETR: 40;

            end;

            b <> e

            proof

              assume b = e;

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

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

              hence contradiction by A43, ANALMETR: 40;

            end;

            hence thesis by A61, A62, A63;

          end;

          then

          consider e be Element of X such that

           A64: LIN (o,e,b) and

           A65: LIN (a,c,e) and

           A66: e <> c and

           A67: e <> b;

          reconsider e9 = e as Element of the AffinStruct of X;

          ex e1 be Element of X st LIN (o,e1,b1) & LIN (a1,c1,e1)

          proof

            consider p be Element of X such that

             A68: (o,b1) // (o,p) and

             A69: o <> p by ANALMETR: 39;

            reconsider p9 = p as Element of the AffinStruct of X;

            consider p1 be Element of X such that

             A70: (a1,c1) // (a1,p1) and

             A71: a1 <> p1 by ANALMETR: 39;

            reconsider p19 = p1 as Element of the AffinStruct of X;

            

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

            proof

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

              then (a1,c1) _|_ (o,b) by A12, A47, ANALMETR: 62;

              hence contradiction by A15, A18, A54, ANALMETR: 63;

            end;

             not (o,p) // (a1,p1)

            proof

              assume (o,p) // (a1,p1);

              then (a1,p1) // (o,b1) by A68, A69, ANALMETR: 60;

              hence contradiction by A70, A71, A72, ANALMETR: 60;

            end;

            then not (o9,p9) // (a19,p19) by ANALMETR: 36;

            then

            consider e19 be Element of the AffinStruct of X such that

             A73: LIN (o9,p9,e19) and

             A74: LIN (a19,p19,e19) by AFF_1: 60;

            reconsider e1 = e19 as Element of X;

             LIN (o,p,e1) by A73, ANALMETR: 40;

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

            then (o,e1) // (o,b1) by A68, A69, ANALMETR: 60;

            then

             A75: LIN (o,e1,b1) by ANALMETR:def 10;

             LIN (a1,p1,e1) by A74, ANALMETR: 40;

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

            then (a1,c1) // (a1,e1) by A70, A71, ANALMETR: 60;

            then LIN (a1,c1,e1) by ANALMETR:def 10;

            hence thesis by A75;

          end;

          then

          consider e1 be Element of X such that

           A76: LIN (o,e1,b1) and

           A77: LIN (a1,c1,e1);

          reconsider e19 = e1 as Element of the AffinStruct of X;

          (o,e) // (o,b) by A64, ANALMETR:def 10;

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

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

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

          then

           A78: (o,b1) _|_ (o,e) by A12, A52, ANALMETR: 62;

          (o,e1) // (o,b1) by A76, ANALMETR:def 10;

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

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

          then

           A79: (o,b1) // (o,e1) by ANALMETR: 36;

          

           A80: o <> e

          proof

            assume o = e;

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

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

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

            hence contradiction by A16, ANALMETR:def 10;

          end;

          

           A81: o <> e1

          proof

            assume o = e1;

            then LIN (a19,c19,o9) by A77, ANALMETR: 40;

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

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

            then (o,a1) // (o,c1) by ANALMETR:def 10;

            then (o,c1) _|_ (o,a) by A11, A45, ANALMETR: 62;

            hence contradiction by A13, A16, A49, ANALMETR: 63;

          end;

          

           A82: (o,e) _|_ (o,e1) by A47, A78, A79, ANALMETR: 62;

          

           A83: not LIN (o,a,e)

          proof

            assume LIN (o,a,e);

            then (o,a) // (o,e) by ANALMETR:def 10;

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

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

            then

             A84: (o,e) // (o,a) by ANALMETR: 36;

            (o,e) // (o,b) by A64, ANALMETR:def 10;

            hence contradiction by A17, A80, A84, ANALMETR: 60;

          end;

          (a,c) // (a,e) by A65, ANALMETR:def 10;

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

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

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

          then

           A85: (a1,c1) _|_ (e,a) by A15, A53, ANALMETR: 62;

          (a1,c1) // (a1,e1) by A77, ANALMETR:def 10;

          then (e,a) _|_ (a1,e1) by A54, A85, ANALMETR: 62;

          then

           A86: (e,a) _|_ (e1,a1) by ANALMETR: 61;

          (b,a) _|_ (b1,a1) by A14, ANALMETR: 61;

          then

           A87: (e,e1) // (b,b1) by A10, A11, A12, A45, A47, A51, A52, A64, A67, A76, A80, A81, A82, A83, A86;

          

           A88: not LIN (o,c,e)

          proof

            assume LIN (o,c,e);

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

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

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

            then

             A89: (c,e) // (c,o) by ANALMETR: 36;

             LIN (a9,c9,e9) by A65, ANALMETR: 40;

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

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

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

            then (c,o) // (c,a) by A66, A89, ANALMETR: 60;

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

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

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

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

            hence contradiction by A16, ANALMETR:def 10;

          end;

           LIN (a9,c9,e9) by A65, ANALMETR: 40;

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

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

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

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

          then

           A90: (a1,c1) _|_ (e,c) by A15, A53, ANALMETR: 62;

           LIN (a19,c19,e19) by A77, ANALMETR: 40;

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

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

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

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

          then (e,c) _|_ (e1,c1) by A54, A90, ANALMETR: 62;

          hence (b,c) _|_ (b1,c1) by A9, A12, A13, A46, A47, A49, A52, A64, A67, A76, A80, A81, A82, A87, A88;

        end;

        hence (b,c) _|_ (b1,c1) by A19, A26, A35;

      end;

      then

       A91: not (o,b) // (a,c) implies (b,c) _|_ (b1,c1) by A1, A2, A3, A4, A5, A6, A7, A8;

       A92:

      now

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

        assume that

         A93: (o,a) _|_ (o,a1) and

         A94: (o,b) _|_ (o,b1) and

         A95: (o,c) _|_ (o,c1) and

         A96: (a,b) _|_ (a1,b1) and

         A97: (a,c) _|_ (a1,c1) and

         A98: not (o,c) // (o,a) and

         A99: not (o,a) // (o,b);

        assume

         A100: not (o,a) // (c,b);

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

         A101:

        now

          assume

           A102: o = a1;

          then

           A103: (a1,b1) _|_ (b,a1) by A94, ANALMETR: 61;

          

           A104: (a1,b1) _|_ (b,a) by A96, ANALMETR: 61;

           not (b,a1) // (b,a)

          proof

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

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

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

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

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

            hence contradiction by A99, ANALMETR:def 10;

          end;

          then

           A105: a1 = b1 by A103, A104, ANALMETR: 63;

          

           A106: (a1,c1) _|_ (c,a1) by A95, A102, ANALMETR: 61;

          (a1,c1) _|_ (c,a) by A97, ANALMETR: 61;

          then

           A107: (c,a1) // (c,a) or a1 = c1 by A106, ANALMETR: 63;

           not (c,a1) // (c,a)

          proof

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

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

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

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

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

            hence contradiction by A98, ANALMETR:def 10;

          end;

          hence (b,c) _|_ (b1,c1) by A105, A107, ANALMETR: 39;

        end;

         A108:

        now

          assume that

           A109: LIN (o,b,c) and

           A110: o <> a1;

          

           A111: o <> b by A99, ANALMETR: 39;

          

           A112: o <> c

          proof

            assume o = c;

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

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

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

            hence contradiction by A98, ANALMETR: 36;

          end;

          

           A113: o <> b1

          proof

            assume

             A114: o = b1;

            (a1,o) _|_ (a,o) by A93, ANALMETR: 61;

            then (a,o) // (a,b) by A96, A110, A114, ANALMETR: 63;

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

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

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

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

            hence contradiction by A99, ANALMETR:def 10;

          end;

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

          then (o,c) _|_ (o,b1) by A94, A111, ANALMETR: 62;

          then (o,b1) // (o,c1) by A95, A112, ANALMETR: 63;

          then LIN (o,b1,c1) by ANALMETR:def 10;

          then LIN (o9,b19,c19) by ANALMETR: 40;

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

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

          then

           A115: (b1,o) // (b1,c1) by ANALMETR:def 10;

          (b1,o) _|_ (b,o) by A94, ANALMETR: 61;

          then

           A116: (b,o) _|_ (b1,c1) by A113, A115, ANALMETR: 62;

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

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

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

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

          hence (b,c) _|_ (b1,c1) by A111, A116, ANALMETR: 62;

        end;

         A117:

        now

          assume that

           A118: LIN (a,b,c) and not LIN (o,b,c) and

           A119: o <> a1;

          

           A120: a <> c

          proof

            assume a = c;

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

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

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

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

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

            hence contradiction by A98, ANALMETR:def 10;

          end;

          

           A121: a <> b

          proof

            assume a = b;

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

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

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

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

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

            hence contradiction by A99, ANALMETR:def 10;

          end;

          

           A122: a1 <> b1 by A93, A94, A99, A119, ANALMETR: 63;

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

          then (a,c) _|_ (a1,b1) by A96, A121, ANALMETR: 62;

          then (a1,b1) // (a1,c1) by A97, A120, ANALMETR: 63;

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

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

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

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

          then

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

          (b1,a1) _|_ (b,a) by A96, ANALMETR: 61;

          then

           A124: (b,a) _|_ (b1,c1) by A122, A123, ANALMETR: 62;

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

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

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

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

          hence (b,c) _|_ (b1,c1) by A121, A124, ANALMETR: 62;

        end;

        now

          assume that

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

           A126: not LIN (o,b,c) and

           A127: o <> a1;

          

           A128: o <> a by A98, ANALMETR: 39;

          

           A129: o <> c

          proof

            assume o = c;

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

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

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

            hence contradiction by A98, ANALMETR: 36;

          end;

          

           A130: o <> b1

          proof

            assume

             A131: o = b1;

            (a1,o) _|_ (a,o) by A93, ANALMETR: 61;

            then (a,o) // (a,b) by A96, A127, A131, ANALMETR: 63;

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

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

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

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

            hence contradiction by A99, ANALMETR:def 10;

          end;

          

           A132: o <> c1

          proof

            assume

             A133: o = c1;

            (a1,o) _|_ (a,o) by A93, ANALMETR: 61;

            then (a,o) // (a,c) by A97, A127, A133, ANALMETR: 63;

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

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

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

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

            hence contradiction by A98, ANALMETR:def 10;

          end;

          

           A134: o <> a by A98, ANALMETR: 39;

          

           A135: o <> b by A99, ANALMETR: 39;

          

           A136: a <> a1 by A93, A128, ANALMETR: 39;

          ex e be Element of X st LIN (b,c,e) & LIN (o,e,a) & c <> e & e <> b & a <> e

          proof

            consider p be Element of X such that

             A137: (o,a) // (o,p) and

             A138: o <> p by ANALMETR: 39;

            reconsider p9 = p as Element of the AffinStruct of X;

            consider p1 be Element of X such that

             A139: (b,c) // (b,p1) and

             A140: b <> p1 by ANALMETR: 39;

            reconsider p19 = p1 as Element of the AffinStruct of X;

             not (o,p) // (b,p1)

            proof

              assume (o,p) // (b,p1);

              then (b,p1) // (o,a) by A137, A138, ANALMETR: 60;

              then (o,a) // (b,c) by A139, A140, ANALMETR: 60;

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

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

              hence contradiction by A100, ANALMETR: 36;

            end;

            then not (o9,p9) // (b9,p19) by ANALMETR: 36;

            then

            consider e9 be Element of the AffinStruct of X such that

             A141: LIN (o9,p9,e9) and

             A142: LIN (b9,p19,e9) by AFF_1: 60;

            reconsider e = e9 as Element of X;

             LIN (o,p,e) by A141, ANALMETR: 40;

            then

             A143: (o,p) // (o,e) by ANALMETR:def 10;

            then (o,e) // (o,a) by A137, A138, ANALMETR: 60;

            then

             A144: LIN (o,e,a) by ANALMETR:def 10;

             LIN (b,p1,e) by A142, ANALMETR: 40;

            then (b,p1) // (b,e) by ANALMETR:def 10;

            then (b,c) // (b,e) by A139, A140, ANALMETR: 60;

            then

             A145: LIN (b,c,e) by ANALMETR:def 10;

            

             A146: c <> e by A98, A137, A138, A143, ANALMETR: 60;

            

             A147: b <> e

            proof

              assume b = e;

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

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

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

              hence contradiction by A99, ANALMETR:def 10;

            end;

            a <> e

            proof

              assume a = e;

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

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

              hence contradiction by A125, ANALMETR: 40;

            end;

            hence thesis by A144, A145, A146, A147;

          end;

          then

          consider e be Element of X such that

           A148: LIN (b,c,e) and

           A149: LIN (o,e,a) and

           A150: e <> b and

           A151: c <> e and

           A152: a <> e;

          reconsider e9 = e as Element of the AffinStruct of X;

          ex e1 be Element of X st LIN (o,e1,a1) & (e,e1) // (a,a1)

          proof

            consider p be Element of X such that

             A153: (o,a1) // (o,p) and

             A154: o <> p by ANALMETR: 39;

            reconsider p9 = p as Element of the AffinStruct of X;

            consider p1 be Element of X such that

             A155: (a,a1) // (e,p1) and

             A156: e <> p1 by ANALMETR: 39;

            reconsider p19 = p1 as Element of the AffinStruct of X;

             not (o,p) // (e,p1)

            proof

              assume (o,p) // (e,p1);

              then (e,p1) // (o,a1) by A153, A154, ANALMETR: 60;

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

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

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

              then (e,p1) _|_ (o,a) by A93, A127, ANALMETR: 62;

              then (o,a) _|_ (a,a1) by A155, A156, ANALMETR: 62;

              then

               A157: (o,a) _|_ (a1,a) by ANALMETR: 61;

              (o,a) _|_ (a1,o) by A93, ANALMETR: 61;

              then (a1,o) // (a1,a) by A134, A157, ANALMETR: 63;

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

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

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

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

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

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

              then (a1,a) _|_ (a1,a) by A134, A157, ANALMETR: 62;

              hence contradiction by A136, ANALMETR: 39;

            end;

            then not (o9,p9) // (e9,p19) by ANALMETR: 36;

            then

            consider e19 be Element of the AffinStruct of X such that

             A158: LIN (o9,p9,e19) and

             A159: LIN (e9,p19,e19) by AFF_1: 60;

            reconsider e1 = e19 as Element of X;

             LIN (o,p,e1) by A158, ANALMETR: 40;

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

            then (o,e1) // (o,a1) by A153, A154, ANALMETR: 60;

            then

             A160: LIN (o,e1,a1) by ANALMETR:def 10;

             LIN (e,p1,e1) by A159, ANALMETR: 40;

            then (e,p1) // (e,e1) by ANALMETR:def 10;

            then (e,e1) // (a,a1) by A155, A156, ANALMETR: 60;

            hence thesis by A160;

          end;

          then

          consider e1 be Element of X such that

           A161: LIN (o,e1,a1) and

           A162: (e,e1) // (a,a1);

          reconsider e19 = e1 as Element of the AffinStruct of X;

          (o,e) // (o,a) by A149, ANALMETR:def 10;

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

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

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

          then

           A163: (o,a1) _|_ (o,e) by A93, A134, ANALMETR: 62;

          (o,e1) // (o,a1) by A161, ANALMETR:def 10;

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

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

          then

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

          

           A165: o <> e

          proof

            assume o = e;

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

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

            hence contradiction by A126, ANALMETR: 40;

          end;

          

           A166: o <> e1

          proof

            assume o = e1;

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

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

            then

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

            (o,e) // (o,a) by A149, ANALMETR:def 10;

            then

             A168: (o,a) // (a,a1) by A165, A167, ANALMETR: 60;

            then

             A169: (o,a1) _|_ (a,a1) by A93, A134, ANALMETR: 62;

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

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

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

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

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

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

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

            then (a,a1) _|_ (a,a1) by A127, A169, ANALMETR: 62;

            hence contradiction by A136, ANALMETR: 39;

          end;

          

           A170: (o,e) _|_ (o,e1) by A127, A163, A164, ANALMETR: 62;

          

           A171: not LIN (o,b,a)

          proof

            assume LIN (o,b,a);

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

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

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

            hence contradiction by A99, ANALMETR: 36;

          end;

          (o,e) // (o,a) by A149, ANALMETR:def 10;

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

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

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

          then

           A172: LIN (o,a,e) by ANALMETR:def 10;

          (o,e1) // (o,a1) by A161, ANALMETR:def 10;

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

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

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

          then

           A173: LIN (o,a1,e1) by ANALMETR:def 10;

          (e9,e19) // (a9,a19) by A162, ANALMETR: 36;

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

          then

           A174: (a,a1) // (e,e1) by ANALMETR: 36;

          then

           A175: (e,b) _|_ (e1,b1) by A9, A93, A94, A96, A127, A130, A134, A135, A152, A165, A166, A170, A171, A172, A173;

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

          then

           A176: (e,c) _|_ (e1,c1) by A9, A93, A95, A97, A127, A129, A132, A134, A152, A165, A166, A170, A172, A173, A174;

          

           A177: e1 <> b1

          proof

            assume e1 = b1;

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

            then (o,a1) _|_ (o,b) by A94, A130, ANALMETR: 62;

            hence contradiction by A93, A99, A127, ANALMETR: 63;

          end;

          

           A178: (c,e) _|_ (c1,e1) by A176, ANALMETR: 61;

          

           A179: LIN (b9,c9,e9) by A148, ANALMETR: 40;

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

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

          then (c,e) // (c,b) by ANALMETR:def 10;

          then

           A180: (c,b) _|_ (c1,e1) by A151, A178, ANALMETR: 62;

          

           A181: c <> b

          proof

            assume c = b;

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

            hence contradiction by A126, ANALMETR: 40;

          end;

          (b9,c9) // (b9,e9) by A179, AFF_1:def 1;

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

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

          then (e,b) _|_ (c1,e1) by A180, A181, ANALMETR: 62;

          then (e1,b1) // (c1,e1) by A150, A175, ANALMETR: 63;

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

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

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

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

          then (b19,e19) // (b19,c19) by AFF_1:def 1;

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

          then

           A182: (e1,b1) // (b1,c1) by ANALMETR: 36;

           LIN (b9,e9,c9) by A179, AFF_1: 6;

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

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

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

          then (e1,b1) _|_ (b,c) by A150, A175, ANALMETR: 62;

          hence (b,c) _|_ (b1,c1) by A177, A182, ANALMETR: 62;

        end;

        hence (b,c) _|_ (b1,c1) by A101, A108, A117;

      end;

      then

       A183: not (o,a) // (c,b) implies (b,c) _|_ (b1,c1) by A2, A3, A4, A5, A6, A7, A8;

      now

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

        assume X is satisfying_LIN;

        assume that

         A184: (o,a) _|_ (o,a1) and

         A185: (o,b) _|_ (o,b1) and

         A186: (o,c) _|_ (o,c1) and

         A187: (a,b) _|_ (a1,b1) and

         A188: (a,c) _|_ (a1,c1) and

         A189: not (o,c) // (o,a) and

         A190: not (o,a) // (o,b);

        assume that

         A191: (o,a) // (c,b) and (o,b) // (a,c);

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

         A192:

        now

          assume

           A193: o = a1;

          then

           A194: (a1,b1) _|_ (b,a1) by A185, ANALMETR: 61;

          

           A195: (a1,b1) _|_ (b,a) by A187, ANALMETR: 61;

           not (b,a1) // (b,a)

          proof

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

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

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

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

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

            hence contradiction by A190, ANALMETR:def 10;

          end;

          then

           A196: a1 = b1 by A194, A195, ANALMETR: 63;

          

           A197: (a1,c1) _|_ (c,a1) by A186, A193, ANALMETR: 61;

          (a1,c1) _|_ (c,a) by A188, ANALMETR: 61;

          then

           A198: (c,a1) // (c,a) or a1 = c1 by A197, ANALMETR: 63;

           not (c,a1) // (c,a)

          proof

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

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

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

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

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

            hence contradiction by A189, ANALMETR:def 10;

          end;

          hence (b,c) _|_ (b1,c1) by A196, A198, ANALMETR: 39;

        end;

         A199:

        now

          assume that

           A200: (o,a1) // (c1,b1) and

           A201: o <> a1;

          o <> a

          proof

            assume o = a;

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

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

            hence contradiction by A189, ANALMETR:def 10;

          end;

          then (c,b) _|_ (o,a1) by A184, A191, ANALMETR: 62;

          then (c,b) _|_ (c1,b1) by A200, A201, ANALMETR: 62;

          hence (b,c) _|_ (b1,c1) by ANALMETR: 61;

        end;

        now

          assume that

           A202: not (o,a1) // (c1,b1) and

           A203: o <> a1;

          

           A204: (o,a1) _|_ (o,a) by A184, ANALMETR: 61;

          

           A205: (o,b1) _|_ (o,b) by A185, ANALMETR: 61;

          

           A206: (o,c1) _|_ (o,c) by A186, ANALMETR: 61;

          

           A207: (a1,b1) _|_ (a,b) by A187, ANALMETR: 61;

          

           A208: (a1,c1) _|_ (a,c) by A188, ANALMETR: 61;

          

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

          proof

            assume

             A210: (o,c1) // (o,a1);

            o <> c1

            proof

              assume o = c1;

              then (a,c) _|_ (o,a1) by A188, ANALMETR: 61;

              then (a,c) // (o,a) by A184, A203, ANALMETR: 63;

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

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

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

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

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

              hence contradiction by A189, ANALMETR:def 10;

            end;

            then (o,c) _|_ (o,a1) by A186, A210, ANALMETR: 62;

            hence contradiction by A184, A189, A203, ANALMETR: 63;

          end;

           not (o,a1) // (o,b1)

          proof

            assume

             A211: (o,a1) // (o,b1);

            

             A212: o <> b1

            proof

              assume o = b1;

              then (a,b) _|_ (o,a1) by A187, ANALMETR: 61;

              then (a,b) // (o,a) by A184, A203, ANALMETR: 63;

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

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

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

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

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

              hence contradiction by A190, ANALMETR:def 10;

            end;

            (o,a) _|_ (o,b1) by A184, A203, A211, ANALMETR: 62;

            hence contradiction by A185, A190, A212, ANALMETR: 63;

          end;

          then (b1,c1) _|_ (b,c) by A92, A202, A204, A205, A206, A207, A208, A209;

          hence (b,c) _|_ (b1,c1) by ANALMETR: 61;

        end;

        hence (b,c) _|_ (b1,c1) by A192, A199;

      end;

      hence thesis by A1, A2, A3, A4, A5, A6, A7, A8, A91, A183;

    end;

    theorem :: CONAFFM:6

    X is satisfying_LIN implies X is satisfying_3H

    proof

      assume

       A1: X is satisfying_LIN;

      let a, b, c;

      assume

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

      consider e1 such that

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

       A4: a <> e1 by ANALMETR:def 9;

      consider e2 such that

       A5: (a,c) _|_ (b,e2) and

       A6: b <> e2 by ANALMETR:def 9;

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

       not (a9,e19) // (b9,e29)

      proof

        assume (a9,e19) // (b9,e29);

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

        then (b,e2) _|_ (b,c) by A3, A4, ANALMETR: 62;

        then (a,c) // (b,c) by A5, A6, ANALMETR: 63;

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

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

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

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

        hence contradiction by A2, ANALMETR: 40;

      end;

      then

      consider d9 be Element of the AffinStruct of X such that

       A7: LIN (a9,e19,d9) and

       A8: LIN (b9,e29,d9) by AFF_1: 60;

      reconsider d = d9 as Element of X;

      take d;

       LIN (b,e2,d) by A8, ANALMETR: 40;

      then

       A9: (b,e2) // (b,d) by ANALMETR:def 10;

      then

       A10: (a,c) _|_ (b,d) by A5, A6, ANALMETR: 62;

      then

       A11: (d,b) _|_ (a,c) by ANALMETR: 61;

       LIN (a,e1,d) by A7, ANALMETR: 40;

      then

       A12: (a,e1) // (a,d) by ANALMETR:def 10;

      then

       A13: (b,c) _|_ (a,d) by A3, A4, ANALMETR: 62;

      then

       A14: (d,a) _|_ (b,c) by ANALMETR: 61;

      

       A15: X is satisfying_LIN1 by A1, Th3;

       A16:

      now

        assume

         A17: d <> c;

        now

          assume

           A18: b <> d;

           not (b9,d9) // (a9,c9)

          proof

            assume (b9,d9) // (a9,c9);

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

            then

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

            a <> c

            proof

              assume a = c;

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

              hence contradiction by A2, ANALMETR: 40;

            end;

            then (b,d) _|_ (b,d) by A10, A19, ANALMETR: 62;

            hence contradiction by A18, ANALMETR: 39;

          end;

          then

          consider o9 be Element of the AffinStruct of X such that

           A20: LIN (b9,d9,o9) and

           A21: LIN (a9,c9,o9) by AFF_1: 60;

          reconsider o = o9 as Element of X;

          now

            assume

             A22: d <> a;

            

             A23: o <> a

            proof

              assume

               A24: o = a;

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

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

              then (b,a) _|_ (a,c) by A10, A18, ANALMETR: 62;

              then

               A25: (a,b) _|_ (a,c) by ANALMETR: 61;

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

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

              then

               A26: (a,b) // (a,d) by ANALMETR:def 10;

              a <> b

              proof

                assume a = b;

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

                hence contradiction by A2, ANALMETR: 40;

              end;

              then (a,d) _|_ (a,c) by A25, A26, ANALMETR: 62;

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

              then (a,c) // (b,c) by A14, A22, ANALMETR: 63;

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

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

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

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

              hence contradiction by A2, ANALMETR: 40;

            end;

            

             A27: c <> o

            proof

              assume

               A28: c = o;

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

              then (b,d) // (b,c) by ANALMETR:def 10;

              then

               A29: (b,c) _|_ (a,c) by A10, A18, ANALMETR: 62;

              b <> c

              proof

                assume b = c;

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

                hence contradiction by A2, ANALMETR: 40;

              end;

              then (a,d) // (a,c) by A13, A29, ANALMETR: 63;

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

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

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

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

              then

               A30: (c,d) // (c,a) by ANALMETR:def 10;

               LIN (c9,d9,b9) by A20, A28, AFF_1: 6;

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

              then (c,d) // (c,b) by ANALMETR:def 10;

              then (c,a) // (c,b) by A17, A30, ANALMETR: 60;

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

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

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

              hence contradiction by A2, ANALMETR: 40;

            end;

            consider e1 such that

             A31: (a,c) // (a,e1) and

             A32: a <> e1 by ANALMETR: 39;

            consider e2 such that

             A33: (b,c) // (d,e2) and

             A34: d <> e2 by ANALMETR: 39;

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

             not (a9,e19) // (d9,e29)

            proof

              assume (a9,e19) // (d9,e29);

              then (a,e1) // (d,e2) by ANALMETR: 36;

              then (d,e2) // (a,c) by A31, A32, ANALMETR: 60;

              then (a,c) // (b,c) by A33, A34, ANALMETR: 60;

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

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

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

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

              hence contradiction by A2, ANALMETR: 40;

            end;

            then

            consider d19 such that

             A35: LIN (a9,e19,d19) and

             A36: LIN (d9,e29,d19) by AFF_1: 60;

            reconsider d1 = d19 as Element of X;

             LIN (a,e1,d1) by A35, ANALMETR: 40;

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

            then

             A37: (a,c) // (a,d1) by A31, A32, ANALMETR: 60;

            then

             A38: LIN (a,c,d1) by ANALMETR:def 10;

             LIN (d,e2,d1) by A36, ANALMETR: 40;

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

            then

             A39: (b,c) // (d,d1) by A33, A34, ANALMETR: 60;

            

             A40: o <> d

            proof

              assume

               A41: o = d;

              then

               A42: (a,o) _|_ (b,c) by A3, A4, A12, ANALMETR: 62;

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

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

              then

               A43: (a,c) _|_ (b,c) by A23, A42, ANALMETR: 62;

              a <> c

              proof

                assume a = c;

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

                hence contradiction by A2, ANALMETR: 40;

              end;

              then (b,o) // (b,c) by A10, A41, A43, ANALMETR: 63;

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

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

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

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

              then

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

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

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

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

              then (c,b) // (c,a) by A27, A44, ANALMETR: 60;

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

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

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

              hence contradiction by A2, ANALMETR: 40;

            end;

            

             A45: o <> d1

            proof

              assume

               A46: o = d1;

               LIN (o9,d9,b9) by A20, AFF_1: 6;

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

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

              then (d,o) // (b,o) by ANALMETR: 59;

              then (b,c) // (b,o) by A39, A40, A46, ANALMETR: 60;

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

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

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

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

              then

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

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

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

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

              then (c,a) // (c,b) by A27, A47, ANALMETR: 60;

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

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

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

              hence contradiction by A2, ANALMETR: 40;

            end;

            

             A48: o <> b

            proof

              assume o = b;

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

              hence contradiction by A2, ANALMETR: 40;

            end;

            

             A49: d1 <> c

            proof

              assume

               A50: d1 = c;

              

               A51: b <> c

              proof

                assume b = c;

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

                hence contradiction by A2, ANALMETR: 40;

              end;

              (c,b) // (c,d) by A39, A50, ANALMETR: 59;

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

              then

               A52: LIN (c9,b9,d9) by ANALMETR: 40;

              (b,c) // (c,d) by A39, A50, ANALMETR: 59;

              then (d,a) _|_ (c,d) by A14, A51, ANALMETR: 62;

              then

               A53: (d,c) _|_ (d,a) by ANALMETR: 61;

               LIN (d9,c9,b9) by A52, AFF_1: 6;

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

              then (d,c) // (d,b) by ANALMETR:def 10;

              then (d,b) _|_ (d,a) by A17, A53, ANALMETR: 62;

              then (a,c) // (d,a) by A11, A18, ANALMETR: 63;

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

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

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

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

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

              then

               A54: (c,a) // (c,d) by ANALMETR:def 10;

              (c,d) // (b,c) by A39, A50, ANALMETR: 59;

              then (c,a) // (b,c) by A17, A54, ANALMETR: 60;

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

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

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

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

              hence contradiction by A2, ANALMETR: 40;

            end;

             LIN (d9,o9,b9) by A20, AFF_1: 6;

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

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

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

            then

             A55: (a,c) _|_ (o,d) by A10, A18, ANALMETR: 62;

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

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

            then

             A56: (a,c) // (o,a) by ANALMETR: 59;

            a <> c

            proof

              assume a = c;

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

              hence contradiction by A2, ANALMETR: 40;

            end;

            then

             A57: (o,d) _|_ (o,a) by A55, A56, ANALMETR: 62;

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

            then

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

            

             A59: a <> c

            proof

              assume a = c;

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

              hence contradiction by A2, ANALMETR: 40;

            end;

            then (a,o) // (a,d1) by A37, A58, ANALMETR: 60;

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

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

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

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

            then

             A60: (o,a) // (o,d1) by ANALMETR:def 10;

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

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

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

            then (a,c) // (o,d1) by A23, A60, ANALMETR: 60;

            then

             A61: (b,d) _|_ (o,d1) by A10, A59, ANALMETR: 62;

             LIN (d9,o9,b9) by A20, AFF_1: 6;

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

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

            then (b,d) // (o,d) by ANALMETR: 59;

            then

             A62: (o,d1) _|_ (o,d) by A18, A61, ANALMETR: 62;

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

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

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

            then

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

            a <> c

            proof

              assume a = c;

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

              hence contradiction by A2, ANALMETR: 40;

            end;

            then

             A64: (b,d) _|_ (o,c) by A10, A63, ANALMETR: 62;

            (b9,d9) // (b9,o9) by A20, AFF_1:def 1;

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

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

            then

             A65: (o,c) _|_ (o,b) by A18, A64, ANALMETR: 62;

            

             A66: not LIN (o,d,d1)

            proof

              assume LIN (o,d,d1);

              then (o,d) // (o,d1) by ANALMETR:def 10;

              then (o,d) _|_ (o,d) by A45, A62, ANALMETR: 62;

              hence contradiction by A40, ANALMETR: 39;

            end;

             LIN (a9,c9,d19) by A38, ANALMETR: 40;

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

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

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

            then

             A67: (a,c) // (c,d1) by ANALMETR: 36;

            

             A68: a <> c

            proof

              assume a = c;

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

              hence contradiction by A2, ANALMETR: 40;

            end;

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

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

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

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

            then (c,d1) // (c,o) by A67, A68, ANALMETR: 60;

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

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

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

            then

             A69: LIN (o,d1,c) by ANALMETR: 40;

             LIN (o9,d9,b9) by A20, AFF_1: 6;

            then

             A70: LIN (o,d,b) by ANALMETR: 40;

            

             A71: (d1,d) // (c,b) by A39, ANALMETR: 59;

            b <> c

            proof

              assume b = c;

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

              hence contradiction by A2, ANALMETR: 40;

            end;

            then (d,d1) _|_ (a,d) by A13, A39, ANALMETR: 62;

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

            then (c,d) _|_ (b,a) by A15, A23, A27, A40, A45, A48, A49, A57, A62, A65, A66, A69, A70, A71;

            hence thesis by A10, A13, ANALMETR: 61;

          end;

          hence thesis by A3, A4, A10, A12, ANALMETR: 61, ANALMETR: 62;

        end;

        hence thesis by A5, A6, A9, A13, ANALMETR: 61, ANALMETR: 62;

      end;

      now

        assume d = c;

        then (a,b) _|_ (d,c) by ANALMETR: 39;

        hence thesis by A10, A13, ANALMETR: 61;

      end;

      hence thesis by A16;

    end;