conmetr1.miz



    begin

    reserve X for AffinPlane;

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

    reserve Y,Z,M,N,A,K,C for Subset of X;

    definition

      let X;

      :: CONMETR1:def1

      attr X is satisfying_minor_Scherungssatz 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);

    end

    definition

      let X;

      :: CONMETR1:def2

      attr X is satisfying_major_Scherungssatz means for o, a1, a2, a3, a4, b1, b2, b3, b4, M, N st M is being_line & N is being_line & o in M & o in 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);

    end

    definition

      let X;

      :: CONMETR1:def3

      attr X is satisfying_Scherungssatz 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);

    end

    definition

      let X;

      :: CONMETR1:def4

      attr X is satisfying_indirect_Scherungssatz 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 & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & (a3,a2) // (b3,b2) & (a2,a1) // (b2,b1) & (a1,a4) // (b1,b4) holds (a3,a4) // (b3,b4);

    end

    definition

      let X;

      :: CONMETR1:def5

      attr X is satisfying_minor_indirect_Scherungssatz 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 a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & (a3,a2) // (b3,b2) & (a2,a1) // (b2,b1) & (a1,a4) // (b1,b4) holds (a3,a4) // (b3,b4);

    end

    definition

      let X;

      :: CONMETR1:def6

      attr X is satisfying_major_indirect_Scherungssatz means for o, a1, a2, a3, a4, b1, b2, b3, b4, M, N st M is being_line & N is being_line & o in M & o in 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 a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & (a3,a2) // (b3,b2) & (a2,a1) // (b2,b1) & (a1,a4) // (b1,b4) holds (a3,a4) // (b3,b4);

    end

    theorem :: CONMETR1:1

    

     Th1: X is satisfying_indirect_Scherungssatz iff X is satisfying_minor_indirect_Scherungssatz & X is satisfying_major_indirect_Scherungssatz

    proof

      

       A1: X is satisfying_indirect_Scherungssatz implies X is satisfying_minor_indirect_Scherungssatz

      proof

        assume

         A2: X is satisfying_indirect_Scherungssatz;

        now

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

          assume that

           A3: M // N and

           A4: a1 in M and

           A5: a3 in M and

           A6: b2 in M and

           A7: b4 in M and

           A8: a2 in N and

           A9: a4 in N and

           A10: b1 in N and

           A11: b3 in N and

           A12: not a4 in M and

           A13: not a2 in M and

           A14: not b1 in M and

           A15: not b3 in M and

           A16: not a1 in N and

           A17: not a3 in N and

           A18: not b2 in N and

           A19: not b4 in N and

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

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

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

          

           A23: N is being_line by A3, AFF_1: 36;

          M is being_line by A3, AFF_1: 36;

          hence (a3,a4) // (b3,b4) by A2, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23;

        end;

        hence thesis;

      end;

      

       A24: X is satisfying_minor_indirect_Scherungssatz & X is satisfying_major_indirect_Scherungssatz implies X is satisfying_indirect_Scherungssatz

      proof

        assume that

         A25: X is satisfying_minor_indirect_Scherungssatz and

         A26: X is satisfying_major_indirect_Scherungssatz;

        now

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

          assume that

           A27: M is being_line and

           A28: N is being_line and

           A29: a1 in M and

           A30: a3 in M and

           A31: b2 in M and

           A32: b4 in M and

           A33: a2 in N and

           A34: a4 in N and

           A35: b1 in N and

           A36: b3 in N and

           A37: not a4 in M and

           A38: not a2 in M and

           A39: not b1 in M and

           A40: not b3 in M and

           A41: not a1 in N and

           A42: not a3 in N and

           A43: not b2 in N and

           A44: not b4 in N and

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

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

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

          now

            assume not M // N;

            then ex o st o in M & o in N by A27, A28, AFF_1: 58;

            hence (a3,a4) // (b3,b4) by A26, A27, A28, A29, A30, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A47;

          end;

          hence (a3,a4) // (b3,b4) by A25, A29, A30, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A47;

        end;

        hence thesis;

      end;

      thus thesis by A1, A24;

    end;

    theorem :: CONMETR1:2

    

     Th2: X is satisfying_Scherungssatz iff X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz

    proof

      

       A1: X is satisfying_Scherungssatz implies X is satisfying_minor_Scherungssatz

      proof

        assume

         A2: X is satisfying_Scherungssatz;

        now

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

          assume that

           A3: M // N and

           A4: a1 in M and

           A5: a3 in M and

           A6: b1 in M and

           A7: b3 in M and

           A8: a2 in N and

           A9: a4 in N and

           A10: b2 in N and

           A11: b4 in N and

           A12: not a4 in M and

           A13: not a2 in M and

           A14: not b2 in M and

           A15: not b4 in M and

           A16: not a1 in N and

           A17: not a3 in N and

           A18: not b1 in N and

           A19: not b3 in N and

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

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

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

          

           A23: N is being_line by A3, AFF_1: 36;

          M is being_line by A3, AFF_1: 36;

          hence (a3,a4) // (b3,b4) by A2, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23;

        end;

        hence thesis;

      end;

      

       A24: X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz implies X is satisfying_Scherungssatz

      proof

        assume that

         A25: X is satisfying_minor_Scherungssatz and

         A26: X is satisfying_major_Scherungssatz;

        now

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

          assume that

           A27: M is being_line and

           A28: N is being_line and

           A29: a1 in M and

           A30: a3 in M and

           A31: b1 in M and

           A32: b3 in M and

           A33: a2 in N and

           A34: a4 in N and

           A35: b2 in N and

           A36: b4 in N and

           A37: not a4 in M and

           A38: not a2 in M and

           A39: not b2 in M and

           A40: not b4 in M and

           A41: not a1 in N and

           A42: not a3 in N and

           A43: not b1 in N and

           A44: not b3 in N and

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

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

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

          now

            assume not M // N;

            then ex o st o in M & o in N by A27, A28, AFF_1: 58;

            hence (a3,a4) // (b3,b4) by A26, A27, A28, A29, A30, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A47;

          end;

          hence (a3,a4) // (b3,b4) by A25, A29, A30, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A47;

        end;

        hence thesis;

      end;

      thus thesis by A1, A24;

    end;

    theorem :: CONMETR1:3

    

     Th3: X is satisfying_minor_indirect_Scherungssatz implies X is satisfying_minor_Scherungssatz

    proof

      assume

       A1: X is satisfying_minor_indirect_Scherungssatz;

      now

        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

         A18: not b3 in N and

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

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

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

        

         A22: N is being_line by A2, AFF_1: 36;

        then

        consider d1 such that a2 <> d1 and

         A23: d1 in N by AFF_1: 20;

        

         A24: not d1 in M by A2, A8, A11, A23, AFF_1: 45;

        

         A25: M is being_line by A2, AFF_1: 36;

        ex d2 st d2 in M & (a2,a1) // (d2,d1)

        proof

          consider e1 such that

           A26: a1 <> e1 and

           A27: e1 in M by A25, AFF_1: 20;

          consider e2 such that

           A28: (a2,a1) // (d1,e2) and

           A29: d1 <> e2 by DIRAF: 40;

           not (a1,e1) // (d1,e2)

          proof

            assume (a1,e1) // (d1,e2);

            then (a1,e1) // (a2,a1) by A28, A29, AFF_1: 5;

            then (a1,e1) // (a1,a2) by AFF_1: 4;

            then LIN (a1,e1,a2) by AFF_1:def 1;

            hence contradiction by A3, A12, A25, A26, A27, AFF_1: 25;

          end;

          then

          consider d2 such that

           A30: LIN (a1,e1,d2) and

           A31: LIN (d1,e2,d2) by AFF_1: 60;

          take d2;

          (d1,e2) // (d1,d2) by A31, AFF_1:def 1;

          then (a2,a1) // (d1,d2) by A28, A29, AFF_1: 5;

          hence thesis by A3, A25, A26, A27, A30, AFF_1: 4, AFF_1: 25;

        end;

        then

        consider d2 such that

         A32: d2 in M and

         A33: (a2,a1) // (d2,d1);

        

         A34: not d2 in N by A2, A8, A11, A32, AFF_1: 45;

        ex d3 st d3 in N & (a3,a2) // (d3,d2)

        proof

          consider e1 such that

           A35: a2 <> e1 and

           A36: e1 in N by A22, AFF_1: 20;

          consider e2 such that

           A37: (a3,a2) // (d2,e2) and

           A38: d2 <> e2 by DIRAF: 40;

           not (a2,e1) // (d2,e2)

          proof

            assume (a2,e1) // (d2,e2);

            then (a2,e1) // (a3,a2) by A37, A38, AFF_1: 5;

            then (a2,e1) // (a2,a3) by AFF_1: 4;

            then LIN (a2,e1,a3) by AFF_1:def 1;

            hence contradiction by A7, A16, A22, A35, A36, AFF_1: 25;

          end;

          then

          consider d3 such that

           A39: LIN (a2,e1,d3) and

           A40: LIN (d2,e2,d3) by AFF_1: 60;

          take d3;

          (d2,e2) // (d2,d3) by A40, AFF_1:def 1;

          then (a3,a2) // (d2,d3) by A37, A38, AFF_1: 5;

          hence thesis by A7, A22, A35, A36, A39, AFF_1: 4, AFF_1: 25;

        end;

        then

        consider d3 such that

         A41: d3 in N and

         A42: (a3,a2) // (d3,d2);

        

         A43: not d3 in M by A2, A8, A11, A41, AFF_1: 45;

        ex d4 st d4 in M & (a1,a4) // (d1,d4)

        proof

          consider e1 such that

           A44: a1 <> e1 and

           A45: e1 in M by A25, AFF_1: 20;

          consider e2 such that

           A46: (a1,a4) // (d1,e2) and

           A47: d1 <> e2 by DIRAF: 40;

           not (a1,e1) // (d1,e2)

          proof

            assume (a1,e1) // (d1,e2);

            then (a1,e1) // (a1,a4) by A46, A47, AFF_1: 5;

            then LIN (a1,e1,a4) by AFF_1:def 1;

            hence contradiction by A3, A11, A25, A44, A45, AFF_1: 25;

          end;

          then

          consider d4 such that

           A48: LIN (a1,e1,d4) and

           A49: LIN (d1,e2,d4) by AFF_1: 60;

          take d4;

          (d1,e2) // (d1,d4) by A49, AFF_1:def 1;

          hence thesis by A3, A25, A44, A45, A46, A47, A48, AFF_1: 5, AFF_1: 25;

        end;

        then

        consider d4 such that

         A50: d4 in M and

         A51: (a1,a4) // (d1,d4);

        

         A52: not d4 in N by A2, A8, A11, A50, AFF_1: 45;

        

         A53: (b2,b1) // (d2,d1) by A3, A12, A20, A33, AFF_1: 5;

        

         A54: (b1,b4) // (d1,d4) by A3, A11, A21, A51, AFF_1: 5;

        (b3,b2) // (d3,d2) by A4, A12, A19, A42, AFF_1: 5;

        then

         A55: (b3,b4) // (d3,d4) by A1, A2, A5, A6, A9, A10, A13, A14, A17, A18, A23, A32, A41, A50, A24, A43, A34, A52, A53, A54;

        (a3,a4) // (d3,d4) by A1, A2, A3, A4, A7, A8, A11, A12, A15, A16, A23, A32, A33, A41, A42, A50, A51, A24, A43, A34, A52;

        hence (a3,a4) // (b3,b4) by A50, A43, A55, AFF_1: 5;

      end;

      hence thesis;

    end;

    theorem :: CONMETR1:4

    

     Th4: X is satisfying_major_indirect_Scherungssatz implies X is satisfying_major_Scherungssatz

    proof

      assume

       A1: X is satisfying_major_indirect_Scherungssatz;

      now

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

        assume that

         A2: M is being_line and

         A3: N is being_line and

         A4: o in M and

         A5: o in N and

         A6: a1 in M and

         A7: a3 in M and

         A8: b1 in M and

         A9: b3 in M and

         A10: a2 in N and

         A11: a4 in N and

         A12: b2 in N and

         A13: b4 in N and

         A14: not a4 in M and

         A15: not a2 in M and

         A16: not b2 in M and

         A17: not b4 in M and

         A18: not a1 in N and

         A19: not a3 in N and

         A20: not b1 in N and

         A21: not b3 in N and

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

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

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

         A25:

        now

          assume that

           A26: a1 <> a3 and

           A27: a2 <> a4;

          consider d1 such that

           A28: o <> d1 and

           A29: d1 in N by A4, A11, A14;

          

           A30: ex d4 st d4 in M & (a1,a4) // (d1,d4)

          proof

            consider e1 such that

             A31: o <> e1 and

             A32: e1 in M by A5, A6, A18;

            consider e2 such that

             A33: (a1,a4) // (d1,e2) and

             A34: d1 <> e2 by DIRAF: 40;

             not (o,e1) // (d1,e2)

            proof

              assume (o,e1) // (d1,e2);

              then

               A35: (o,e1) // (a1,a4) by A33, A34, AFF_1: 5;

              (o,e1) // (a1,a3) by A2, A4, A6, A7, A32, AFF_1: 39, AFF_1: 41;

              then (a1,a3) // (a1,a4) by A31, A35, AFF_1: 5;

              then LIN (a1,a3,a4) by AFF_1:def 1;

              hence contradiction by A2, A6, A7, A14, A26, AFF_1: 25;

            end;

            then

            consider d4 such that

             A36: LIN (o,e1,d4) and

             A37: LIN (d1,e2,d4) by AFF_1: 60;

            take d4;

            (d1,e2) // (d1,d4) by A37, AFF_1:def 1;

            hence thesis by A2, A4, A31, A32, A33, A34, A36, AFF_1: 5, AFF_1: 25;

          end;

          

           A38: ex d2 st d2 in M & (a2,a1) // (d2,d1)

          proof

            consider e1 such that

             A39: o <> e1 and

             A40: e1 in M by A5, A6, A18;

            consider e2 such that

             A41: (a2,a1) // (d1,e2) and

             A42: d1 <> e2 by DIRAF: 40;

             not (o,e1) // (d1,e2)

            proof

              assume (o,e1) // (d1,e2);

              then

               A43: (o,e1) // (a2,a1) by A41, A42, AFF_1: 5;

              (o,e1) // (a1,a3) by A2, A4, A6, A7, A40, AFF_1: 39, AFF_1: 41;

              then (a1,a3) // (a2,a1) by A39, A43, AFF_1: 5;

              then (a1,a3) // (a1,a2) by AFF_1: 4;

              then LIN (a1,a3,a2) by AFF_1:def 1;

              hence contradiction by A2, A6, A7, A15, A26, AFF_1: 25;

            end;

            then

            consider d2 such that

             A44: LIN (o,e1,d2) and

             A45: LIN (d1,e2,d2) by AFF_1: 60;

            take d2;

            (d1,e2) // (d1,d2) by A45, AFF_1:def 1;

            then (a2,a1) // (d1,d2) by A41, A42, AFF_1: 5;

            hence thesis by A2, A4, A39, A40, A44, AFF_1: 4, AFF_1: 25;

          end;

          consider d4 such that

           A46: d4 in M and

           A47: (a1,a4) // (d1,d4) by A30;

          consider d2 such that

           A48: d2 in M and

           A49: (a2,a1) // (d2,d1) by A38;

          

           A50: (b2,b1) // (d2,d1) by A6, A15, A23, A49, AFF_1: 5;

          ex d3 st d3 in N & (a3,a2) // (d3,d2)

          proof

            consider e1 such that

             A51: o <> e1 and

             A52: e1 in N by A4, A11, A14;

            consider e2 such that

             A53: (a3,a2) // (d2,e2) and

             A54: d2 <> e2 by DIRAF: 40;

             not (o,e1) // (d2,e2)

            proof

              assume (o,e1) // (d2,e2);

              then

               A55: (o,e1) // (a3,a2) by A53, A54, AFF_1: 5;

              (o,e1) // (a2,a4) by A3, A5, A10, A11, A52, AFF_1: 39, AFF_1: 41;

              then (a2,a4) // (a3,a2) by A51, A55, AFF_1: 5;

              then (a2,a4) // (a2,a3) by AFF_1: 4;

              then LIN (a2,a4,a3) by AFF_1:def 1;

              hence contradiction by A3, A10, A11, A19, A27, AFF_1: 25;

            end;

            then

            consider d3 such that

             A56: LIN (o,e1,d3) and

             A57: LIN (d2,e2,d3) by AFF_1: 60;

            take d3;

            (d2,e2) // (d2,d3) by A57, AFF_1:def 1;

            then (a3,a2) // (d2,d3) by A53, A54, AFF_1: 5;

            hence thesis by A3, A5, A51, A52, A56, AFF_1: 4, AFF_1: 25;

          end;

          then

          consider d3 such that

           A58: d3 in N and

           A59: (a3,a2) // (d3,d2);

          

           A60: d2 <> o & d3 <> o & d4 <> o

          proof

             A61:

            now

              assume

               A62: d4 = o;

              (d1,o) // (a2,a4) by A3, A5, A10, A11, A29, AFF_1: 39, AFF_1: 41;

              then (a1,a4) // (a2,a4) by A28, A47, A62, AFF_1: 5;

              then (a4,a2) // (a4,a1) by AFF_1: 4;

              then LIN (a4,a2,a1) by AFF_1:def 1;

              hence contradiction by A3, A10, A11, A18, A27, AFF_1: 25;

            end;

             A63:

            now

              assume

               A64: d2 = o;

              (o,d1) // (a2,a4) by A3, A5, A10, A11, A29, AFF_1: 39, AFF_1: 41;

              then (a2,a4) // (a2,a1) by A28, A49, A64, AFF_1: 5;

              then LIN (a2,a4,a1) by AFF_1:def 1;

              hence contradiction by A3, A10, A11, A18, A27, AFF_1: 25;

            end;

             A65:

            now

              assume

               A66: d3 = o;

              (o,d2) // (a3,a1) by A2, A4, A6, A7, A48, AFF_1: 39, AFF_1: 41;

              then (a3,a1) // (a3,a2) by A59, A63, A66, AFF_1: 5;

              then LIN (a3,a1,a2) by AFF_1:def 1;

              hence contradiction by A2, A6, A7, A15, A26, AFF_1: 25;

            end;

            assume not thesis;

            hence contradiction by A63, A65, A61;

          end;

          

           A67: not d1 in M & not d3 in M & not d2 in N & not d4 in N

          proof

            assume not thesis;

            then

             A68: (o,d1) // M or (o,d3) // M or (o,d2) // N or (o,d4) // N by A2, A3, A4, A5, AFF_1: 52;

            

             A69: (o,d3) // N by A3, A5, A58, AFF_1: 52;

            

             A70: (o,d4) // M by A2, A4, A46, AFF_1: 52;

            

             A71: (o,d2) // M by A2, A4, A48, AFF_1: 52;

            (o,d1) // N by A3, A5, A29, AFF_1: 52;

            hence contradiction by A4, A5, A11, A14, A28, A60, A68, A69, A71, A70, AFF_1: 45, AFF_1: 53;

          end;

          

           A72: (b1,b4) // (d1,d4) by A6, A14, A24, A47, AFF_1: 5;

          

           A73: d1 <> d2 & d2 <> d3 & d3 <> d4 & d4 <> d1

          proof

            assume not thesis;

            then

             A74: (o,d1) // M or (o,d3) // M by A2, A4, A48, A46, AFF_1: 52;

            

             A75: (o,d3) // N by A3, A5, A58, AFF_1: 52;

            (o,d1) // N by A3, A5, A29, AFF_1: 52;

            hence contradiction by A4, A5, A11, A14, A28, A60, A74, A75, AFF_1: 45, AFF_1: 53;

          end;

          (b3,b2) // (d3,d2) by A7, A15, A22, A59, AFF_1: 5;

          then

           A76: (b3,b4) // (d3,d4) by A1, A2, A3, A4, A5, A8, A9, A12, A13, A16, A17, A20, A21, A29, A48, A58, A46, A67, A50, A72;

          (a3,a4) // (d3,d4) by A1, A2, A3, A4, A5, A6, A7, A10, A11, A14, A15, A18, A19, A29, A48, A49, A58, A59, A46, A47, A67;

          hence (a3,a4) // (b3,b4) by A73, A76, AFF_1: 5;

        end;

        now

           A77:

          now

            (o,b2) // (o,b4) by A3, A5, A12, A13, AFF_1: 39, AFF_1: 41;

            then

             A78: LIN (o,b2,b4) by AFF_1:def 1;

            assume

             A79: a2 = a4;

            then (a1,a4) // (b1,b2) by A23, AFF_1: 4;

            then (b1,b2) // (b1,b4) by A6, A14, A24, AFF_1: 5;

            hence (a3,a4) // (b3,b4) by A2, A4, A5, A8, A16, A20, A22, A79, A78, AFF_1: 14, AFF_1: 25;

          end;

           A80:

          now

            (o,b1) // (o,b3) by A2, A4, A8, A9, AFF_1: 39, AFF_1: 41;

            then

             A81: LIN (o,b1,b3) by AFF_1:def 1;

            assume

             A82: a1 = a3;

            then (a2,a1) // (b2,b3) by A22, AFF_1: 4;

            then (b2,b1) // (b2,b3) by A6, A15, A23, AFF_1: 5;

            hence (a3,a4) // (b3,b4) by A3, A4, A5, A12, A16, A20, A24, A82, A81, AFF_1: 14, AFF_1: 25;

          end;

          assume a1 = a3 or a2 = a4;

          hence (a3,a4) // (b3,b4) by A80, A77;

        end;

        hence (a3,a4) // (b3,b4) by A25;

      end;

      hence thesis;

    end;

    theorem :: CONMETR1:5

    X is satisfying_indirect_Scherungssatz implies X is satisfying_Scherungssatz

    proof

      assume

       A1: X is satisfying_indirect_Scherungssatz;

      then X is satisfying_major_indirect_Scherungssatz;

      then

       A2: X is satisfying_major_Scherungssatz by Th4;

      X is satisfying_minor_indirect_Scherungssatz by A1, Th1;

      then X is satisfying_minor_Scherungssatz by Th3;

      hence thesis by A2, Th2;

    end;

    theorem :: CONMETR1:6

    

     Th6: X is translational implies X is satisfying_minor_Scherungssatz

    proof

      assume

       A1: X is translational;

      now

        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 not b4 in M and

         A14: not a1 in N and

         A15: not a3 in N and

         A16: not b1 in N and not b3 in N and

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

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

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

        

         A20: M is being_line by A2, AFF_1: 36;

        

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

         A22:

        now

          assume that

           A23: a1 <> a3 and

           A24: a2 <> a4;

           A25:

          now

            assume ex x, y, z st LIN (x,y,z) & x <> y & x <> z & y <> z;

            then

            consider d such that

             A26: LIN (a1,a2,d) and

             A27: a1 <> d and

             A28: a2 <> d by TRANSLAC: 1;

            

             A29: ex Y st Y is being_line & d in Y & Y // M

            proof

              consider Y such that

               A30: d in Y and

               A31: M // Y by A20, AFF_1: 49;

              take Y;

              thus thesis by A30, A31, AFF_1: 36;

            end;

             LIN (a2,a1,d) by A26, AFF_1: 6;

            then (a2,a1) // (a2,d) by AFF_1:def 1;

            then

             A32: (b2,b1) // (a2,d) by A3, A12, A18, AFF_1: 5;

            

             A33: (a2,a3) // (b2,b3) by A17, AFF_1: 4;

            consider Y such that

             A34: Y is being_line and

             A35: d in Y and

             A36: Y // M by A29;

            

             A37: Y // N by A2, A36, AFF_1: 44;

            

             A38: N <> M & N <> Y & Y <> M

            proof

               A39:

              now

                 LIN (a2,d,a1) by A26, AFF_1: 6;

                then

                 A40: (a2,d) // (a2,a1) by AFF_1:def 1;

                assume N = Y;

                then (a2,d) // (a2,a4) by A7, A8, A34, A35, AFF_1: 39, AFF_1: 41;

                then (a2,a4) // (a2,a1) by A28, A40, AFF_1: 5;

                then LIN (a2,a4,a1) by AFF_1:def 1;

                hence contradiction by A7, A8, A14, A21, A24, AFF_1: 25;

              end;

               A41:

              now

                assume Y = M;

                then

                 A42: (a1,d) // (a1,a3) by A3, A4, A35, A36, AFF_1: 39;

                (a1,a2) // (a1,d) by A26, AFF_1:def 1;

                then (a1,a3) // (a1,a2) by A27, A42, AFF_1: 5;

                then LIN (a1,a3,a2) by AFF_1:def 1;

                hence contradiction by A3, A4, A12, A20, A23, AFF_1: 25;

              end;

              assume not thesis;

              hence contradiction by A8, A11, A39, A41;

            end;

            

             A43: Y // Y by A34, AFF_1: 41;

            ex d1 st d1 in Y & (b1,b2) // (b1,d1)

            proof

              consider e1 such that

               A44: d <> e1 and

               A45: e1 in Y by A34, AFF_1: 20;

              consider e2 such that

               A46: (b1,b2) // (b1,e2) and

               A47: b1 <> e2 by DIRAF: 40;

               not (d,e1) // (b1,e2)

              proof

                assume (d,e1) // (b1,e2);

                then (d,e1) // (b1,b2) by A46, A47, AFF_1: 5;

                then

                 A48: (b1,b2) // Y by A35, A43, A44, A45, AFF_1: 32, AFF_1: 40;

                (a1,a3) // Y by A3, A4, A36, AFF_1: 40;

                then (a1,a3) // (b1,b2) by A34, A48, AFF_1: 31;

                then (a1,a3) // (b2,b1) by AFF_1: 4;

                then (a1,a3) // (a2,a1) by A5, A13, A18, AFF_1: 5;

                then (a1,a3) // (a1,a2) by AFF_1: 4;

                then LIN (a1,a3,a2) by AFF_1:def 1;

                hence contradiction by A3, A4, A12, A20, A23, AFF_1: 25;

              end;

              then

              consider d1 such that

               A49: LIN (d,e1,d1) and

               A50: LIN (b1,e2,d1) by AFF_1: 60;

              take d1;

              (b1,e2) // (b1,d1) by A50, AFF_1:def 1;

              hence thesis by A34, A35, A44, A45, A46, A47, A49, AFF_1: 5, AFF_1: 25;

            end;

            then

            consider d1 such that

             A51: d1 in Y and

             A52: (b1,b2) // (b1,d1);

            (a1,a2) // (a1,d) by A26, AFF_1:def 1;

            then (a2,a1) // (a1,d) by AFF_1: 4;

            then (b2,b1) // (a1,d) by A3, A12, A18, AFF_1: 5;

            then (b1,b2) // (a1,d) by AFF_1: 4;

            then (a1,d) // (b1,d1) by A5, A13, A52, AFF_1: 5;

            then

             A53: (d,a4) // (d1,b4) by A1, A2, A3, A5, A8, A10, A19, A20, A21, A34, A35, A36, A51, A38, AFF_2:def 11;

             LIN (b1,b2,d1) by A52, AFF_1:def 1;

            then LIN (b2,b1,d1) by AFF_1: 6;

            then (b2,b1) // (b2,d1) by AFF_1:def 1;

            then

             A54: (a2,d) // (b2,d1) by A5, A13, A32, AFF_1: 5;

            N // Y by A2, A36, AFF_1: 44;

            then (d,a3) // (d1,b3) by A1, A2, A4, A6, A7, A9, A20, A21, A34, A35, A51, A38, A54, A33, AFF_2:def 11;

            hence (a3,a4) // (b3,b4) by A1, A4, A6, A8, A10, A20, A21, A34, A35, A36, A51, A38, A53, A37, AFF_2:def 11;

          end;

          now

            assume

             A55: not ex x, y, z st LIN (x,y,z) & x <> y & x <> z & y <> z;

             A56:

            now

              assume

               A57: a1 = b1;

              then

               A58: LIN (a1,a4,b4) by A19, AFF_1:def 1;

              (a1,a2) // (a1,b2) by A18, A57, AFF_1: 4;

              then

               A59: LIN (a1,a2,b2) by AFF_1:def 1;

              (a2,b2) // M by A2, A7, A9, AFF_1: 40;

              then a2 = b2 by A3, A12, A59, AFF_1: 46;

              then (a2,a3) // (a2,b3) by A17, AFF_1: 4;

              then

               A60: LIN (a2,a3,b3) by AFF_1:def 1;

              (a3,b3) // N by A2, A4, A6, AFF_1: 40;

              then

               A61: a3 = b3 by A7, A15, A60, AFF_1: 46;

              (a4,b4) // M by A2, A8, A10, AFF_1: 40;

              then a4 = b4 by A3, A11, A58, AFF_1: 46;

              hence (a3,a4) // (b3,b4) by A61, AFF_1: 2;

            end;

             A62:

            now

              assume

               A63: a3 = b1;

               A64:

              now

                

                 A65: a4 <> b4

                proof

                  assume a4 = b4;

                  then (a4,a1) // (a4,b1) by A19, AFF_1: 4;

                  then

                   A66: LIN (a4,a1,b1) by AFF_1:def 1;

                  (a1,b1) // N by A2, A3, A5, AFF_1: 40;

                  hence contradiction by A8, A14, A23, A63, A66, AFF_1: 46;

                end;

                (a2,a4) // (a2,b4) by A7, A8, A10, A21, AFF_1: 39, AFF_1: 41;

                then LIN (a2,a4,b4) by AFF_1:def 1;

                then

                 A67: a2 = b4 by A24, A55, A65;

                assume

                 A68: a4 = b2;

                

                 A69: a3 <> b3

                proof

                  assume a3 = b3;

                  then

                   A70: LIN (a3,a2,b2) by A17, AFF_1:def 1;

                  (a2,b2) // M by A2, A7, A9, AFF_1: 40;

                  hence contradiction by A4, A12, A24, A68, A70, AFF_1: 46;

                end;

                (a1,a3) // (a1,b3) by A3, A4, A6, A20, AFF_1: 39, AFF_1: 41;

                then LIN (a1,a3,b3) by AFF_1:def 1;

                then

                 A71: a1 = b3 by A23, A55, A69;

                (a3,a4) // (b2,b1) by A63, A68, AFF_1: 2;

                then (a3,a4) // (a2,a1) by A5, A13, A18, AFF_1: 5;

                hence (a3,a4) // (b3,b4) by A71, A67, AFF_1: 4;

              end;

               A72:

              now

                assume a2 = b2;

                then

                 A73: LIN (a2,a1,b1) by A18, AFF_1:def 1;

                (a1,b1) // N by A2, A3, A5, AFF_1: 40;

                hence (a3,a4) // (b3,b4) by A7, A14, A56, A73, AFF_1: 46;

              end;

              (a2,a4) // (a2,b2) by A7, A8, A9, A21, AFF_1: 39, AFF_1: 41;

              then LIN (a2,a4,b2) by AFF_1:def 1;

              hence (a3,a4) // (b3,b4) by A24, A55, A64, A72;

            end;

            (a1,a3) // (a1,b1) by A3, A4, A5, A20, AFF_1: 39, AFF_1: 41;

            then LIN (a1,a3,b1) by AFF_1:def 1;

            hence (a3,a4) // (b3,b4) by A23, A55, A56, A62;

          end;

          hence (a3,a4) // (b3,b4) by A25;

        end;

        now

           A74:

          now

            assume

             A75: a1 = a3;

            b1 = b3

            proof

               LIN (a2,a1,a3) by A75, AFF_1: 7;

              then (a2,a1) // (a2,a3) by AFF_1:def 1;

              then (b2,b1) // (a2,a3) by A3, A12, A18, AFF_1: 5;

              then (b2,b1) // (a3,a2) by AFF_1: 4;

              then (b2,b1) // (b3,b2) by A4, A12, A17, AFF_1: 5;

              then (b2,b1) // (b2,b3) by AFF_1: 4;

              then

               A76: LIN (b2,b1,b3) by AFF_1:def 1;

              assume

               A77: b1 <> b3;

              (b1,b3) // N by A2, A5, A6, AFF_1: 40;

              hence contradiction by A9, A16, A77, A76, AFF_1: 46;

            end;

            hence (a3,a4) // (b3,b4) by A19, A75;

          end;

           A78:

          now

            assume

             A79: a2 = a4;

            then LIN (a1,a4,a2) by AFF_1: 7;

            then (a1,a4) // (a1,a2) by AFF_1:def 1;

            then (b1,b4) // (a1,a2) by A3, A11, A19, AFF_1: 5;

            then (b1,b4) // (a2,a1) by AFF_1: 4;

            then (b1,b4) // (b2,b1) by A3, A12, A18, AFF_1: 5;

            then (b1,b2) // (b1,b4) by AFF_1: 4;

            then

             A80: LIN (b1,b2,b4) by AFF_1:def 1;

            (b2,b4) // M by A2, A9, A10, AFF_1: 40;

            hence (a3,a4) // (b3,b4) by A5, A13, A17, A79, A80, AFF_1: 46;

          end;

          assume a1 = a3 or a2 = a4;

          hence (a3,a4) // (b3,b4) by A74, A78;

        end;

        hence (a3,a4) // (b3,b4) by A22;

      end;

      hence thesis;

    end;

    theorem :: CONMETR1:7

    

     Th7: X is Desarguesian implies X is satisfying_major_Scherungssatz

    proof

      assume

       A1: X is Desarguesian;

      now

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

        assume that

         A2: M is being_line and

         A3: N is being_line and

         A4: o in M and

         A5: o in N and

         A6: a1 in M and

         A7: a3 in M and

         A8: b1 in M and

         A9: b3 in M and

         A10: a2 in N and

         A11: a4 in N and

         A12: b2 in N and

         A13: b4 in N and

         A14: not a4 in M and

         A15: not a2 in M and

         A16: not b2 in M and not b4 in M and

         A17: not a1 in N and

         A18: not a3 in N and

         A19: not b1 in N and not b3 in N and

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

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

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

         A23:

        now

           A24:

          now

            assume ex x, y, z st LIN (x,y,z) & x <> y & x <> z & y <> z;

            then

            consider d such that

             A25: LIN (a1,a2,d) and

             A26: a1 <> d and

             A27: a2 <> d by TRANSLAC: 1;

             LIN (o,d,d) by AFF_1: 7;

            then

            consider Y such that

             A28: Y is being_line and

             A29: o in Y and

             A30: d in Y and d in Y by AFF_1: 21;

            (a1,a2) // (a1,d) by A25, AFF_1:def 1;

            then (a2,a1) // (a1,d) by AFF_1: 4;

            then

             A31: (b2,b1) // (a1,d) by A6, A15, A21, AFF_1: 5;

            

             A32: N <> M & N <> Y & M <> Y

            proof

               A33:

              now

                

                 A34: LIN (a1,d,a2) by A25, AFF_1: 6;

                assume

                 A35: N = Y or M = Y;

                 LIN (a2,d,a1) by A25, AFF_1: 6;

                hence contradiction by A2, A3, A6, A10, A15, A17, A26, A27, A30, A35, A34, AFF_1: 25;

              end;

              assume not thesis;

              hence contradiction by A11, A14, A33;

            end;

            

             A36: ex d1 st LIN (b1,b2,d1) & d1 in Y

            proof

               not (b1,b2) // (o,d)

              proof

                

                 A37: o <> d

                proof

                  assume o = d;

                  then LIN (o,a1,a2) by A25, AFF_1: 6;

                  hence contradiction by A2, A4, A5, A6, A15, A17, AFF_1: 25;

                end;

                assume (b1,b2) // (o,d);

                then (b2,b1) // (o,d) by AFF_1: 4;

                then

                 A38: (a2,a1) // (o,d) by A8, A16, A21, AFF_1: 5;

                (a1,a2) // (a1,d) by A25, AFF_1:def 1;

                then (a2,a1) // (a1,d) by AFF_1: 4;

                then (a1,d) // (o,d) by A6, A15, A38, AFF_1: 5;

                then (d,o) // (d,a1) by AFF_1: 4;

                then LIN (d,o,a1) by AFF_1:def 1;

                then LIN (o,d,a1) by AFF_1: 6;

                then (o,d) // (o,a1) by AFF_1:def 1;

                then

                 A39: Y // M by A2, A4, A5, A6, A17, A28, A29, A30, A37, AFF_1: 38;

                 LIN (a2,a1,d) by A25, AFF_1: 6;

                then (a2,a1) // (a2,d) by AFF_1:def 1;

                then (a2,d) // (o,d) by A6, A15, A38, AFF_1: 5;

                then (d,a2) // (d,o) by AFF_1: 4;

                then LIN (d,a2,o) by AFF_1:def 1;

                then LIN (o,d,a2) by AFF_1: 6;

                then (o,d) // (o,a2) by AFF_1:def 1;

                then Y // N by A3, A4, A5, A10, A15, A28, A29, A30, A37, AFF_1: 38;

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

                hence contradiction by A4, A5, A11, A14, AFF_1: 45;

              end;

              then

              consider d1 such that

               A40: LIN (b1,b2,d1) and

               A41: LIN (o,d,d1) by AFF_1: 60;

              take d1;

              o <> d

              proof

                assume o = d;

                then LIN (o,a1,a2) by A25, AFF_1: 6;

                hence contradiction by A2, A4, A5, A6, A15, A17, AFF_1: 25;

              end;

              hence thesis by A28, A29, A30, A40, A41, AFF_1: 25;

            end;

             LIN (a2,a1,d) by A25, AFF_1: 6;

            then (a2,a1) // (a2,d) by AFF_1:def 1;

            then

             A42: (b2,b1) // (a2,d) by A6, A15, A21, AFF_1: 5;

            

             A43: o <> d

            proof

              assume o = d;

              then LIN (o,a1,a2) by A25, AFF_1: 6;

              hence contradiction by A2, A4, A5, A6, A15, A17, AFF_1: 25;

            end;

            consider d1 such that

             A44: LIN (b1,b2,d1) and

             A45: d1 in Y by A36;

            (b1,b2) // (b1,d1) by A44, AFF_1:def 1;

            then (b2,b1) // (b1,d1) by AFF_1: 4;

            then (a1,d) // (b1,d1) by A8, A16, A31, AFF_1: 5;

            then

             A46: (d,a4) // (d1,b4) by A1, A2, A3, A4, A5, A6, A8, A11, A13, A14, A17, A22, A28, A29, A30, A45, A43, A32, AFF_2:def 4;

             LIN (b2,b1,d1) by A44, AFF_1: 6;

            then (b2,b1) // (b2,d1) by AFF_1:def 1;

            then

             A47: (a2,d) // (b2,d1) by A8, A16, A42, AFF_1: 5;

            (a2,a3) // (b2,b3) by A20, AFF_1: 4;

            then (d,a3) // (d1,b3) by A1, A2, A3, A4, A5, A7, A9, A10, A12, A15, A18, A28, A29, A30, A45, A43, A32, A47, AFF_2:def 4;

            hence (a3,a4) // (b3,b4) by A1, A2, A3, A4, A5, A7, A9, A11, A13, A14, A18, A28, A29, A30, A45, A43, A32, A46, AFF_2:def 4;

          end;

          assume that

           A48: a1 <> a3 and

           A49: a2 <> a4;

          now

            assume

             A50: not ex x, y, z st LIN (x,y,z) & x <> y & x <> z & y <> z;

             A51:

            now

              assume

               A52: a1 = b1;

              

               A53: a2 <> b4

              proof

                assume a2 = b4;

                then LIN (a1,a4,a2) by A22, A52, AFF_1:def 1;

                then LIN (a2,a4,a1) by AFF_1: 6;

                hence contradiction by A3, A10, A11, A17, A49, AFF_1: 25;

              end;

              

               A54: a1 <> b3

              proof

                assume a1 = b3;

                then (b2,b1) // (a2,a3) by A20, A52, AFF_1: 4;

                then

                 A55: (a2,a1) // (a2,a3) by A8, A16, A21, AFF_1: 5;

                 LIN (o,a1,a3) by A2, A4, A6, A7, AFF_1: 21;

                hence contradiction by A3, A4, A5, A10, A15, A17, A48, A55, AFF_1: 14, AFF_1: 25;

              end;

               LIN (a2,a4,b4) by A3, A10, A11, A13, AFF_1: 21;

              then

               A56: a2 = b4 or a4 = b4 by A49, A50;

               LIN (a1,a3,b3) by A2, A6, A7, A9, AFF_1: 21;

              then a3 = b3 by A48, A50, A54;

              hence (a3,a4) // (b3,b4) by A56, A53, AFF_1: 2;

            end;

             A57:

            now

              assume

               A58: a3 = b1;

              

               A59: a2 <> b2

              proof

                assume a2 = b2;

                then LIN (a2,a1,a3) by A21, A58, AFF_1:def 1;

                then LIN (a1,a3,a2) by AFF_1: 6;

                hence contradiction by A2, A6, A7, A15, A48, AFF_1: 25;

              end;

              

               A60: a3 <> b3

              proof

                assume a3 = b3;

                then (a3,a2) // (b2,b1) by A20, A58, AFF_1: 4;

                then (a3,a2) // (a2,a1) by A8, A16, A21, AFF_1: 5;

                then (a2,a3) // (a2,a1) by AFF_1: 4;

                then LIN (a2,a3,a1) by AFF_1:def 1;

                then LIN (a1,a3,a2) by AFF_1: 6;

                hence contradiction by A2, A6, A7, A15, A48, AFF_1: 25;

              end;

              

               A61: a4 <> b4

              proof

                assume a4 = b4;

                then (a4,a1) // (a4,a3) by A22, A58, AFF_1: 4;

                then LIN (a4,a1,a3) by AFF_1:def 1;

                then LIN (a1,a3,a4) by AFF_1: 6;

                hence contradiction by A2, A6, A7, A14, A48, AFF_1: 25;

              end;

               LIN (a2,a4,b4) by A3, A10, A11, A13, AFF_1: 21;

              then

               A62: a2 = b4 by A49, A50, A61;

               LIN (a2,a4,b2) by A3, A10, A11, A12, AFF_1: 21;

              then a4 = b2 by A49, A50, A59;

              then

               A63: (a3,a4) // (b2,b1) by A58, AFF_1: 2;

               LIN (a1,a3,b3) by A2, A6, A7, A9, AFF_1: 21;

              then a1 = b3 by A48, A50, A60;

              then (a3,a4) // (b4,b3) by A8, A16, A21, A62, A63, AFF_1: 5;

              hence (a3,a4) // (b3,b4) by AFF_1: 4;

            end;

             LIN (a1,a3,b1) by A2, A6, A7, A8, AFF_1: 21;

            hence (a3,a4) // (b3,b4) by A48, A50, A51, A57;

          end;

          hence (a3,a4) // (b3,b4) by A24;

        end;

        now

           A64:

          now

            (o,b2) // (o,b4) by A3, A5, A12, A13, AFF_1: 39, AFF_1: 41;

            then

             A65: LIN (o,b2,b4) by AFF_1:def 1;

            assume

             A66: a2 = a4;

            (a1,a2) // (b1,b2) by A21, AFF_1: 4;

            then (b1,b2) // (b1,b4) by A6, A14, A22, A66, AFF_1: 5;

            hence (a3,a4) // (b3,b4) by A2, A4, A5, A8, A16, A19, A20, A66, A65, AFF_1: 14, AFF_1: 25;

          end;

           A67:

          now

            (o,b1) // (o,b3) by A2, A4, A8, A9, AFF_1: 39, AFF_1: 41;

            then

             A68: LIN (o,b1,b3) by AFF_1:def 1;

            assume

             A69: a1 = a3;

            then (a2,a1) // (b2,b3) by A20, AFF_1: 4;

            then (b2,b1) // (b2,b3) by A6, A15, A21, AFF_1: 5;

            hence (a3,a4) // (b3,b4) by A3, A4, A5, A12, A16, A19, A22, A69, A68, AFF_1: 14, AFF_1: 25;

          end;

          assume a1 = a3 or a2 = a4;

          hence (a3,a4) // (b3,b4) by A67, A64;

        end;

        hence (a3,a4) // (b3,b4) by A23;

      end;

      hence thesis;

    end;

    theorem :: CONMETR1:8

    X is Desarguesian iff X is satisfying_Scherungssatz

    proof

      

       A1: X is satisfying_Scherungssatz implies X is Desarguesian

      proof

        assume

         A2: X is satisfying_Scherungssatz;

        now

          let Y, Z, M, o, a, b, c, a1, b1, c1;

          assume that

           A3: o in Y and

           A4: o in Z and

           A5: o in M and

           A6: o <> a and

           A7: o <> b and

           A8: o <> c and

           A9: a in Y and

           A10: a1 in Y and

           A11: b in Z and

           A12: b1 in Z and

           A13: c in M and

           A14: c1 in M and

           A15: Y is being_line and

           A16: Z is being_line and

           A17: M is being_line and

           A18: Y <> Z and

           A19: Y <> M and

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

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

          assume

           A22: not (b,c) // (b1,c1);

           A23:

          now

            let Y, Z, M, o, a, b, c, a1, b1, c1, d;

            assume

             A24: X is satisfying_Scherungssatz;

            assume that

             A25: o in Y and

             A26: o in Z and

             A27: o in M and

             A28: o <> a and

             A29: o <> b and

             A30: o <> c and

             A31: a in Y and

             A32: a1 in Y and

             A33: b in Z and

             A34: b1 in Z and

             A35: c in M and

             A36: c1 in M and

             A37: Y is being_line and

             A38: Z is being_line and

             A39: M is being_line and

             A40: Y <> Z and

             A41: Y <> M and

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

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

             A44: LIN (b,c,d) and

             A45: LIN (b1,c1,d);

             LIN (a,a1,d) or (b,c) // (b1,c1)

            proof

              assume that

               A46: not LIN (a,a1,d) and

               A47: not (b,c) // (b1,c1);

              

               A48: c <> c1 & a <> a1 & b <> b1

              proof

                 A49:

                now

                  

                   A50: not LIN (o,a,c)

                  proof

                    assume LIN (o,a,c);

                    then c in Y by A25, A28, A31, A37, AFF_1: 25;

                    then

                     A51: (o,c) // Y by A25, A37, AFF_1: 52;

                    (o,c) // M by A27, A35, A39, AFF_1: 52;

                    hence contradiction by A25, A27, A30, A41, A51, AFF_1: 45, AFF_1: 53;

                  end;

                  (o,c) // (o,c1) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                  then

                   A52: LIN (o,c,c1) by AFF_1:def 1;

                  

                   A53: not LIN (o,b,a)

                  proof

                    assume LIN (o,b,a);

                    then a in Z by A26, A29, A33, A38, AFF_1: 25;

                    then

                     A54: (o,a) // Z by A26, A38, AFF_1: 52;

                    (o,a) // Y by A25, A31, A37, AFF_1: 52;

                    hence contradiction by A25, A26, A28, A40, A54, AFF_1: 45, AFF_1: 53;

                  end;

                  (o,a) // (o,a1) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                  then

                   A55: LIN (o,a,a1) by AFF_1:def 1;

                  assume

                   A56: b = b1;

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

                  then a = a1 by A53, A55, AFF_1: 14;

                  then c = c1 by A43, A50, A52, AFF_1: 14;

                  hence contradiction by A47, A56, AFF_1: 2;

                end;

                 A57:

                now

                  

                   A58: not LIN (o,a,b)

                  proof

                    assume LIN (o,a,b);

                    then b in Y by A25, A28, A31, A37, AFF_1: 25;

                    then

                     A59: (o,b) // Y by A25, A37, AFF_1: 52;

                    (o,b) // Z by A26, A33, A38, AFF_1: 52;

                    hence contradiction by A25, A26, A29, A40, A59, AFF_1: 45, AFF_1: 53;

                  end;

                  (o,b) // (o,b1) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                  then

                   A60: LIN (o,b,b1) by AFF_1:def 1;

                  

                   A61: not LIN (o,c,a)

                  proof

                    assume LIN (o,c,a);

                    then a in M by A27, A30, A35, A39, AFF_1: 25;

                    then

                     A62: (o,a) // M by A27, A39, AFF_1: 52;

                    (o,a) // Y by A25, A31, A37, AFF_1: 52;

                    hence contradiction by A25, A27, A28, A41, A62, AFF_1: 45, AFF_1: 53;

                  end;

                  (o,a) // (o,a1) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                  then

                   A63: LIN (o,a,a1) by AFF_1:def 1;

                  assume

                   A64: c = c1;

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

                  then a = a1 by A61, A63, AFF_1: 14;

                  then b = b1 by A42, A58, A60, AFF_1: 14;

                  hence contradiction by A47, A64, AFF_1: 2;

                end;

                 A65:

                now

                  

                   A66: not LIN (o,a,c)

                  proof

                    assume LIN (o,a,c);

                    then c in Y by A25, A28, A31, A37, AFF_1: 25;

                    then

                     A67: (o,c) // Y by A25, A37, AFF_1: 52;

                    (o,c) // M by A27, A35, A39, AFF_1: 52;

                    hence contradiction by A25, A27, A30, A41, A67, AFF_1: 45, AFF_1: 53;

                  end;

                  

                   A68: not LIN (o,a,b)

                  proof

                    assume LIN (o,a,b);

                    then b in Y by A25, A28, A31, A37, AFF_1: 25;

                    then

                     A69: (o,b) // Y by A25, A37, AFF_1: 52;

                    (o,b) // Z by A26, A33, A38, AFF_1: 52;

                    hence contradiction by A25, A26, A29, A40, A69, AFF_1: 45, AFF_1: 53;

                  end;

                  assume

                   A70: a = a1;

                  (o,c) // (o,c1) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                  then LIN (o,c,c1) by AFF_1:def 1;

                  then

                   A71: c = c1 by A43, A70, A66, AFF_1: 14;

                  (o,b) // (o,b1) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                  then LIN (o,b,b1) by AFF_1:def 1;

                  then b = b1 by A42, A70, A68, AFF_1: 14;

                  hence contradiction by A47, A71, AFF_1: 2;

                end;

                assume not thesis;

                hence contradiction by A57, A65, A49;

              end;

              now

                assume

                 A72: b <> c;

                 A73:

                now

                  assume

                   A74: b1 <> o;

                  

                   A75: a1 <> b1 & a1 <> c1

                  proof

                     A76:

                    now

                      

                       A77: o <> a1

                      proof

                        

                         A78: not LIN (a,b,o)

                        proof

                          assume LIN (a,b,o);

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

                          then b in Y by A25, A28, A31, A37, AFF_1: 25;

                          then

                           A79: (o,b) // Y by A25, A37, AFF_1: 52;

                          (o,b) // Z by A26, A33, A38, AFF_1: 52;

                          hence contradiction by A25, A26, A29, A40, A79, AFF_1: 45, AFF_1: 53;

                        end;

                        

                         A80: (o,b) // (o,b1) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                        assume o = a1;

                        then (a,b) // (o,b) by A42, A74, A80, AFF_1: 5;

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

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

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

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

                        then (o,a) // (o,b1) by A29, A80, AFF_1: 5;

                        then LIN (o,a,b1) by AFF_1:def 1;

                        then

                         A81: LIN (a,o,b1) by AFF_1: 6;

                        (b,o) // (b,b1) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                        hence contradiction by A74, A78, A81, AFF_1: 14;

                      end;

                      assume a1 = c1;

                      then

                       A82: (o,a1) // M by A27, A36, A39, AFF_1: 52;

                      (o,a1) // Y by A25, A32, A37, AFF_1: 52;

                      hence contradiction by A25, A27, A41, A82, A77, AFF_1: 45, AFF_1: 53;

                    end;

                     A83:

                    now

                      assume a1 = b1;

                      then

                       A84: (o,b1) // Y by A25, A32, A37, AFF_1: 52;

                      (o,b1) // Z by A26, A34, A38, AFF_1: 52;

                      hence contradiction by A25, A26, A40, A74, A84, AFF_1: 45, AFF_1: 53;

                    end;

                    assume not thesis;

                    hence contradiction by A83, A76;

                  end;

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

                  then

                  consider C such that

                   A85: C is being_line and

                   A86: o in C and o in C and

                   A87: a in C by AFF_1: 21;

                  

                   A88: ex d2 st d2 in C & (a,c) // (d,d2)

                  proof

                    consider e2 such that

                     A89: (a,c) // (d,e2) and

                     A90: d <> e2 by DIRAF: 40;

                    consider e1 such that

                     A91: (o,a) // (o,e1) and

                     A92: o <> e1 by DIRAF: 40;

                     LIN (o,a,e1) by A91, AFF_1:def 1;

                    then

                     A93: e1 in C by A28, A85, A86, A87, AFF_1: 25;

                     not (o,e1) // (d,e2)

                    proof

                      assume (o,e1) // (d,e2);

                      then (o,a) // (d,e2) by A91, A92, AFF_1: 5;

                      then (o,a) // (a,c) by A89, A90, AFF_1: 5;

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

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

                      then c in Y by A25, A28, A31, A37, AFF_1: 25;

                      then

                       A94: (o,c) // Y by A25, A37, AFF_1: 52;

                      (o,c) // M by A27, A35, A39, AFF_1: 52;

                      hence contradiction by A25, A27, A30, A41, A94, AFF_1: 45, AFF_1: 53;

                    end;

                    then

                    consider d2 such that

                     A95: LIN (o,e1,d2) and

                     A96: LIN (d,e2,d2) by AFF_1: 60;

                    take d2;

                    (d,e2) // (d,d2) by A96, AFF_1:def 1;

                    hence thesis by A85, A86, A92, A89, A90, A95, A93, AFF_1: 5, AFF_1: 25;

                  end;

                  

                   A97: ex d1 st d1 in C & (c,c1) // (d,d1)

                  proof

                    consider e2 such that

                     A98: (c,c1) // (d,e2) and

                     A99: d <> e2 by DIRAF: 40;

                    consider e1 such that

                     A100: (o,a) // (o,e1) and

                     A101: o <> e1 by DIRAF: 40;

                     LIN (o,a,e1) by A100, AFF_1:def 1;

                    then

                     A102: e1 in C by A28, A85, A86, A87, AFF_1: 25;

                     not (o,e1) // (d,e2)

                    proof

                      assume (o,e1) // (d,e2);

                      then (o,a) // (d,e2) by A100, A101, AFF_1: 5;

                      then

                       A103: (o,a) // (c,c1) by A98, A99, AFF_1: 5;

                      (c,c1) // (o,c) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                      then (o,a) // (o,c) by A48, A103, AFF_1: 5;

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

                      then c in Y by A25, A28, A31, A37, AFF_1: 25;

                      then

                       A104: (o,c) // Y by A25, A37, AFF_1: 52;

                      (o,c) // M by A27, A35, A39, AFF_1: 52;

                      hence contradiction by A25, A27, A30, A41, A104, AFF_1: 45, AFF_1: 53;

                    end;

                    then

                    consider d1 such that

                     A105: LIN (o,e1,d1) and

                     A106: LIN (d,e2,d1) by AFF_1: 60;

                    take d1;

                    (d,e2) // (d,d1) by A106, AFF_1:def 1;

                    hence thesis by A85, A86, A101, A98, A99, A105, A102, AFF_1: 5, AFF_1: 25;

                  end;

                  consider d2 such that

                   A107: d2 in C and

                   A108: (a,c) // (d,d2) by A88;

                  consider d1 such that

                   A109: d1 in C and

                   A110: (c,c1) // (d,d1) by A97;

                  (c,c1) // (c,o) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                  then

                   A111: (c,o) // (d,d1) by A48, A110, AFF_1: 5;

                  (o,a) // (o,a1) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                  then LIN (o,a,a1) by AFF_1:def 1;

                  then

                   A112: a1 in C by A28, A85, A86, A87, AFF_1: 25;

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

                  then

                  consider A such that

                   A113: A is being_line and

                   A114: b in A and b in A and

                   A115: c in A by AFF_1: 21;

                  

                   A116: d in A by A44, A72, A113, A114, A115, AFF_1: 25;

                  

                   A117: b <> c by A47, AFF_1: 3;

                  

                   A118: ex d3 st d3 in A & (o,b) // (d1,d3)

                  proof

                    consider e2 such that

                     A119: (o,b) // (d1,e2) and

                     A120: d1 <> e2 by DIRAF: 40;

                    consider e1 such that

                     A121: (b,c) // (b,e1) and

                     A122: b <> e1 by DIRAF: 40;

                     LIN (b,c,e1) by A121, AFF_1:def 1;

                    then

                     A123: e1 in A by A117, A113, A114, A115, AFF_1: 25;

                     not (b,e1) // (d1,e2)

                    proof

                      assume (b,e1) // (d1,e2);

                      then (b,c) // (d1,e2) by A121, A122, AFF_1: 5;

                      then

                       A124: (b,c) // (o,b) by A119, A120, AFF_1: 5;

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

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

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

                      then

                       A125: (o,b) // (o,c) by AFF_1:def 1;

                      

                       A126: (o,b) // (o,b1) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                      (o,c) // (o,c1) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                      then (o,b) // (o,c1) by A30, A125, AFF_1: 5;

                      then (o,b1) // (o,c1) by A29, A126, AFF_1: 5;

                      then LIN (o,b1,c1) by AFF_1:def 1;

                      then LIN (b1,c1,o) by AFF_1: 6;

                      then (b1,c1) // (b1,o) by AFF_1:def 1;

                      then (b1,c1) // (o,b1) by AFF_1: 4;

                      then (b1,c1) // (o,b) by A74, A126, AFF_1: 5;

                      hence contradiction by A29, A47, A124, AFF_1: 5;

                    end;

                    then

                    consider d3 such that

                     A127: LIN (b,e1,d3) and

                     A128: LIN (d1,e2,d3) by AFF_1: 60;

                    take d3;

                    (d1,e2) // (d1,d3) by A128, AFF_1:def 1;

                    hence thesis by A113, A114, A122, A119, A120, A127, A123, AFF_1: 5, AFF_1: 25;

                  end;

                  

                   A129: not o in A & not a in A & not d1 in A & not d2 in A

                  proof

                     A130:

                    now

                      

                       A131: a <> b

                      proof

                        assume a = b;

                        then

                         A132: (o,b) // Y by A25, A31, A37, AFF_1: 52;

                        (o,b) // Z by A26, A33, A38, AFF_1: 52;

                        hence contradiction by A25, A26, A29, A40, A132, AFF_1: 45, AFF_1: 53;

                      end;

                      

                       A133: a1 <> b1

                      proof

                        assume a1 = b1;

                        then

                         A134: (o,b1) // Y by A25, A32, A37, AFF_1: 52;

                        (o,b1) // Z by A26, A34, A38, AFF_1: 52;

                        hence contradiction by A25, A26, A40, A74, A134, AFF_1: 45, AFF_1: 53;

                      end;

                      assume a in A;

                      then

                       A135: (a,b) // (a,c) by A113, A114, A115, AFF_1: 39, AFF_1: 41;

                      a <> c

                      proof

                        assume a = c;

                        then

                         A136: (o,c) // Y by A25, A31, A37, AFF_1: 52;

                        (o,c) // M by A27, A35, A39, AFF_1: 52;

                        hence contradiction by A25, A27, A30, A41, A136, AFF_1: 45, AFF_1: 53;

                      end;

                      then (a,b) // (a1,c1) by A43, A135, AFF_1: 5;

                      then (a1,b1) // (a1,c1) by A42, A131, AFF_1: 5;

                      then LIN (a1,b1,c1) by AFF_1:def 1;

                      then LIN (b1,c1,a1) by AFF_1: 6;

                      then (b1,c1) // (b1,a1) by AFF_1:def 1;

                      then

                       A137: (a1,b1) // (b1,c1) by AFF_1: 4;

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

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

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

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

                      then (b,c) // (a1,b1) by A42, A131, AFF_1: 5;

                      hence contradiction by A47, A137, A133, AFF_1: 5;

                    end;

                     A138:

                    now

                      

                       A139: d <> d2

                      proof

                        (o,a) // (o,a1) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                        then LIN (o,a,a1) by AFF_1:def 1;

                        then

                         A140: a1 in C by A28, A85, A86, A87, AFF_1: 25;

                        assume d = d2;

                        then (a,a1) // (a,d) by A85, A87, A107, A140, AFF_1: 39, AFF_1: 41;

                        hence contradiction by A46, AFF_1:def 1;

                      end;

                      assume

                       A141: d2 in A;

                      

                       A142: (d,d2) // (c,a) by A108, AFF_1: 4;

                      d in A by A44, A117, A113, A114, A115, AFF_1: 25;

                      hence contradiction by A113, A115, A130, A141, A139, A142, AFF_1: 48;

                    end;

                     A143:

                    now

                      assume o in A;

                      then

                       A144: (o,b) // (o,c) by A113, A114, A115, AFF_1: 39, AFF_1: 41;

                      

                       A145: (o,b) // (o,b1) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                      (o,c) // (o,c1) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                      then (o,b) // (o,c1) by A30, A144, AFF_1: 5;

                      then (o,b1) // (o,c1) by A29, A145, AFF_1: 5;

                      then LIN (o,b1,c1) by AFF_1:def 1;

                      then LIN (b1,c1,o) by AFF_1: 6;

                      then (b1,c1) // (b1,o) by AFF_1:def 1;

                      then (b1,c1) // (o,b1) by AFF_1: 4;

                      then (o,b) // (b1,c1) by A74, A145, AFF_1: 5;

                      then

                       A146: (b,o) // (b1,c1) by AFF_1: 4;

                       LIN (o,b,c) by A144, AFF_1:def 1;

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

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

                      hence contradiction by A29, A47, A146, AFF_1: 5;

                    end;

                     A147:

                    now

                      

                       A148: d <> d1

                      proof

                        (o,a) // (o,a1) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                        then LIN (o,a,a1) by AFF_1:def 1;

                        then

                         A149: a1 in C by A28, A85, A86, A87, AFF_1: 25;

                        assume d = d1;

                        then (a,a1) // (a,d) by A85, A87, A109, A149, AFF_1: 39, AFF_1: 41;

                        hence contradiction by A46, AFF_1:def 1;

                      end;

                      assume

                       A150: d1 in A;

                      (c,c1) // (c,o) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                      then

                       A151: LIN (c,c1,o) by AFF_1:def 1;

                      

                       A152: (d,d1) // (c,c1) by A110, AFF_1: 4;

                      d in A by A44, A117, A113, A114, A115, AFF_1: 25;

                      then c1 in A by A113, A115, A150, A148, A152, AFF_1: 48;

                      hence contradiction by A48, A113, A115, A143, A151, AFF_1: 25;

                    end;

                    assume not thesis;

                    hence contradiction by A143, A130, A147, A138;

                  end;

                   LIN (b1,b1,c1) by AFF_1: 7;

                  then

                  consider K such that

                   A153: K is being_line and

                   A154: b1 in K and b1 in K and

                   A155: c1 in K by AFF_1: 21;

                  b1 <> c1 by A47, AFF_1: 3;

                  then

                   A156: d in K by A45, A153, A154, A155, AFF_1: 25;

                  consider d3 such that

                   A157: d3 in A and

                   A158: (o,b) // (d1,d3) by A118;

                  

                   A159: b1 <> c1 by A47, AFF_1: 3;

                  ex d4 st d4 in K & (d1,d3) // (d1,d4)

                  proof

                    consider e2 such that

                     A160: (d1,d3) // (d1,e2) and

                     A161: d1 <> e2 by DIRAF: 40;

                    consider e1 such that

                     A162: (b1,c1) // (b1,e1) and

                     A163: b1 <> e1 by DIRAF: 40;

                     LIN (b1,c1,e1) by A162, AFF_1:def 1;

                    then

                     A164: e1 in K by A159, A153, A154, A155, AFF_1: 25;

                     not (b1,e1) // (d1,e2)

                    proof

                      

                       A165: o <> c1

                      proof

                        

                         A166: not LIN (a,c,o)

                        proof

                          assume LIN (a,c,o);

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

                          then c in Y by A25, A28, A31, A37, AFF_1: 25;

                          then

                           A167: (o,c) // Y by A25, A37, AFF_1: 52;

                          (o,c) // M by A27, A35, A39, AFF_1: 52;

                          hence contradiction by A25, A27, A30, A41, A167, AFF_1: 45, AFF_1: 53;

                        end;

                        assume

                         A168: o = c1;

                        (a1,o) // (a,a1) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                        then (a,c) // (a,a1) by A43, A75, A168, AFF_1: 5;

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

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

                        then

                         A169: (a1,c) // (a1,a) by AFF_1:def 1;

                        (a1,a) // (a1,o) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                        then (a1,c) // (a1,o) by A48, A169, AFF_1: 5;

                        then LIN (a1,c,o) by AFF_1:def 1;

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

                        then

                         A170: (c,o) // (c,a1) by AFF_1:def 1;

                        (a,o) // (a,a1) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                        then LIN (a,o,a1) by AFF_1:def 1;

                        hence contradiction by A75, A168, A166, A170, AFF_1: 14;

                      end;

                      

                       A171: d1 <> d3

                      proof

                        

                         A172: d <> d1

                        proof

                          (o,a) // (o,a1) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                          then LIN (o,a,a1) by AFF_1:def 1;

                          then

                           A173: a1 in C by A28, A85, A86, A87, AFF_1: 25;

                          assume d = d1;

                          then (a,a1) // (a,d) by A85, A87, A109, A173, AFF_1: 39, AFF_1: 41;

                          hence contradiction by A46, AFF_1:def 1;

                        end;

                        assume

                         A174: d1 = d3;

                        (c,c1) // (o,c) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                        then (o,c) // (d,d1) by A48, A110, AFF_1: 5;

                        then

                         A175: (d,d1) // (c,o) by AFF_1: 4;

                        

                         A176: (o,b) // (o,b1) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                        d in A by A44, A117, A113, A114, A115, AFF_1: 25;

                        then o in A by A113, A115, A157, A174, A172, A175, AFF_1: 48;

                        then

                         A177: (o,b) // (o,c) by A113, A114, A115, AFF_1: 39, AFF_1: 41;

                        (o,c) // (o,c1) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                        then (o,b) // (o,c1) by A30, A177, AFF_1: 5;

                        then (o,b1) // (o,c1) by A29, A176, AFF_1: 5;

                        then LIN (o,b1,c1) by AFF_1:def 1;

                        then LIN (b1,c1,o) by AFF_1: 6;

                        then (b1,c1) // (b1,o) by AFF_1:def 1;

                        then (b1,c1) // (o,b1) by AFF_1: 4;

                        then

                         A178: (o,b) // (b1,c1) by A74, A176, AFF_1: 5;

                         LIN (o,b,c) by A177, AFF_1:def 1;

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

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

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

                        hence contradiction by A29, A47, A178, AFF_1: 5;

                      end;

                      assume (b1,e1) // (d1,e2);

                      then (b1,c1) // (d1,e2) by A162, A163, AFF_1: 5;

                      then

                       A179: (b1,c1) // (d1,d3) by A160, A161, AFF_1: 5;

                      

                       A180: (o,b) // (o,b1) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                      then (o,b1) // (d1,d3) by A29, A158, AFF_1: 5;

                      then

                       A181: (o,b1) // (b1,c1) by A179, A171, AFF_1: 5;

                      then (b1,o) // (b1,c1) by AFF_1: 4;

                      then LIN (b1,o,c1) by AFF_1:def 1;

                      then LIN (o,b1,c1) by AFF_1: 6;

                      then (o,b1) // (o,c1) by AFF_1:def 1;

                      then

                       A182: (o,b) // (o,c1) by A74, A180, AFF_1: 5;

                      (o,c) // (o,c1) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                      then (o,b) // (o,c) by A182, A165, AFF_1: 5;

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

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

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

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

                      then (o,b1) // (b,c) by A29, A180, AFF_1: 5;

                      hence contradiction by A47, A74, A181, AFF_1: 5;

                    end;

                    then

                    consider d4 such that

                     A183: LIN (b1,e1,d4) and

                     A184: LIN (d1,e2,d4) by AFF_1: 60;

                    take d4;

                    (d1,e2) // (d1,d4) by A184, AFF_1:def 1;

                    hence thesis by A153, A154, A163, A160, A161, A183, A164, AFF_1: 5, AFF_1: 25;

                  end;

                  then

                  consider d4 such that

                   A185: d4 in K and

                   A186: (d1,d3) // (d1,d4);

                  

                   A187: not c in C & not b in C & not d in C & not d3 in C

                  proof

                     A188:

                    now

                      assume b in C;

                      then (o,a) // (o,b) by A85, A86, A87, AFF_1: 39, AFF_1: 41;

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

                      then b in Y by A25, A28, A31, A37, AFF_1: 25;

                      then

                       A189: (o,b) // Y by A25, A37, AFF_1: 52;

                      (o,b) // Z by A26, A33, A38, AFF_1: 52;

                      hence contradiction by A25, A26, A29, A40, A189, AFF_1: 45, AFF_1: 53;

                    end;

                     A190:

                    now

                      

                       A191: d1 <> d3

                      proof

                        

                         A192: d <> d1

                        proof

                          (o,a) // (o,a1) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                          then LIN (o,a,a1) by AFF_1:def 1;

                          then

                           A193: a1 in C by A28, A85, A86, A87, AFF_1: 25;

                          assume d = d1;

                          then (a,a1) // (a,d) by A85, A87, A109, A193, AFF_1: 39, AFF_1: 41;

                          hence contradiction by A46, AFF_1:def 1;

                        end;

                        assume

                         A194: d1 = d3;

                        

                         A195: (o,c) // (o,c1) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                        

                         A196: (d,d1) // (c,c1) by A110, AFF_1: 4;

                        d in A by A44, A117, A113, A114, A115, AFF_1: 25;

                        then c1 in A by A113, A115, A157, A194, A192, A196, AFF_1: 48;

                        then

                         A197: (c,c1) // (c,b) by A113, A114, A115, AFF_1: 39, AFF_1: 41;

                        

                         A198: (o,b) // (o,b1) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                        (c,o) // (c,c1) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                        then (c,o) // (c,b) by A48, A197, AFF_1: 5;

                        then

                         A199: LIN (c,o,b) by AFF_1:def 1;

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

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

                        then (o,b1) // (o,c) by A29, A198, AFF_1: 5;

                        then (o,b1) // (o,c1) by A30, A195, AFF_1: 5;

                        then LIN (o,b1,c1) by AFF_1:def 1;

                        then LIN (b1,c1,o) by AFF_1: 6;

                        then (b1,c1) // (b1,o) by AFF_1:def 1;

                        then (b1,c1) // (o,b1) by AFF_1: 4;

                        then

                         A200: (o,b) // (b1,c1) by A74, A198, AFF_1: 5;

                         LIN (b,c,o) by A199, AFF_1: 6;

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

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

                        hence contradiction by A29, A47, A200, AFF_1: 5;

                      end;

                      assume

                       A201: d3 in C;

                      (d1,d3) // (o,b) by A158, AFF_1: 4;

                      hence contradiction by A85, A86, A109, A188, A201, A191, AFF_1: 48;

                    end;

                     A202:

                    now

                      assume c in C;

                      then (o,a) // (o,c) by A85, A86, A87, AFF_1: 39, AFF_1: 41;

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

                      then c in Y by A25, A28, A31, A37, AFF_1: 25;

                      then

                       A203: (o,c) // Y by A25, A37, AFF_1: 52;

                      (o,c) // M by A27, A35, A39, AFF_1: 52;

                      hence contradiction by A25, A27, A30, A41, A203, AFF_1: 45, AFF_1: 53;

                    end;

                     A204:

                    now

                      assume d in C;

                      then

                       A205: (o,a) // (a,d) by A85, A86, A87, AFF_1: 39, AFF_1: 41;

                      (o,a) // (a,a1) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                      then (a,a1) // (a,d) by A28, A205, AFF_1: 5;

                      hence contradiction by A46, AFF_1:def 1;

                    end;

                    assume not thesis;

                    hence contradiction by A202, A188, A204, A190;

                  end;

                  

                   A206: d4 <> d3

                  proof

                    assume

                     A207: d4 = d3;

                    d = d3

                    proof

                      d in A by A44, A117, A113, A114, A115, AFF_1: 25;

                      then

                       A208: (b,c) // (d,d3) by A113, A114, A115, A157, AFF_1: 39, AFF_1: 41;

                      d in K by A45, A159, A153, A154, A155, AFF_1: 25;

                      then

                       A209: (b1,c1) // (d,d3) by A153, A154, A155, A185, A207, AFF_1: 39, AFF_1: 41;

                      assume d <> d3;

                      hence contradiction by A47, A209, A208, AFF_1: 5;

                    end;

                    then

                     A210: (o,b) // (d,d1) by A158, AFF_1: 4;

                    (o,c) // (c,c1) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                    then (o,c) // (d,d1) by A48, A110, AFF_1: 5;

                    then

                     A211: (o,b) // (o,c) by A109, A187, A210, AFF_1: 5;

                    

                     A212: (o,c) // (o,c1) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                    

                     A213: (o,b) // (o,b1) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                    then (o,b1) // (o,c) by A29, A211, AFF_1: 5;

                    then (o,b1) // (o,c1) by A30, A212, AFF_1: 5;

                    then LIN (o,b1,c1) by AFF_1:def 1;

                    then LIN (b1,c1,o) by AFF_1: 6;

                    then (b1,c1) // (b1,o) by AFF_1:def 1;

                    then (b1,c1) // (o,b1) by AFF_1: 4;

                    then

                     A214: (o,b) // (b1,c1) by A74, A213, AFF_1: 5;

                     LIN (o,b,c) by A211, AFF_1:def 1;

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

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

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

                    hence contradiction by A29, A47, A214, AFF_1: 5;

                  end;

                  

                   A215: a <> b & a <> c

                  proof

                     A216:

                    now

                      assume a = c;

                      then

                       A217: (o,a) // M by A27, A35, A39, AFF_1: 52;

                      (o,a) // Y by A25, A31, A37, AFF_1: 52;

                      hence contradiction by A25, A27, A28, A41, A217, AFF_1: 45, AFF_1: 53;

                    end;

                     A218:

                    now

                      assume a = b;

                      then

                       A219: (o,a) // Z by A26, A33, A38, AFF_1: 52;

                      (o,a) // Y by A25, A31, A37, AFF_1: 52;

                      hence contradiction by A25, A26, A28, A40, A219, AFF_1: 45, AFF_1: 53;

                    end;

                    assume not thesis;

                    hence contradiction by A218, A216;

                  end;

                  

                   A220: not o in K & not a1 in K & not d1 in K & not d2 in K

                  proof

                     A221:

                    now

                      

                       A222: o <> c1

                      proof

                        

                         A223: a1 <> o

                        proof

                          

                           A224: not LIN (a,b,o)

                          proof

                            assume LIN (a,b,o);

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

                            then b in Y by A25, A28, A31, A37, AFF_1: 25;

                            then

                             A225: (o,b) // Y by A25, A37, AFF_1: 52;

                            (o,b) // Z by A26, A33, A38, AFF_1: 52;

                            hence contradiction by A25, A26, A29, A40, A225, AFF_1: 45, AFF_1: 53;

                          end;

                          

                           A226: (o,b) // (o,b1) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                          assume a1 = o;

                          then (a,b) // (o,b) by A42, A74, A226, AFF_1: 5;

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

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

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

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

                          then (o,a) // (o,b1) by A29, A226, AFF_1: 5;

                          then LIN (o,a,b1) by AFF_1:def 1;

                          then

                           A227: LIN (a,o,b1) by AFF_1: 6;

                          (b,o) // (b,b1) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                          hence contradiction by A74, A224, A227, AFF_1: 14;

                        end;

                        

                         A228: not LIN (c,a,o)

                        proof

                          assume LIN (c,a,o);

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

                          then c in Y by A25, A28, A31, A37, AFF_1: 25;

                          then

                           A229: (o,c) // Y by A25, A37, AFF_1: 52;

                          (o,c) // M by A27, A35, A39, AFF_1: 52;

                          hence contradiction by A25, A27, A30, A41, A229, AFF_1: 45, AFF_1: 53;

                        end;

                        

                         A230: (a1,o) // (o,a) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                        assume o = c1;

                        then (a,c) // (o,a) by A43, A223, A230, AFF_1: 5;

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

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

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

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

                        then (o,c) // (a1,o) by A28, A230, AFF_1: 5;

                        then (o,c) // (o,a1) by AFF_1: 4;

                        then LIN (o,c,a1) by AFF_1:def 1;

                        then

                         A231: LIN (c,o,a1) by AFF_1: 6;

                        (a,o) // (a,a1) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                        hence contradiction by A223, A228, A231, AFF_1: 14;

                      end;

                      

                       A232: (o,c) // (o,c1) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                      assume o in K;

                      then

                       A233: (o,b1) // (o,c1) by A153, A154, A155, AFF_1: 39, AFF_1: 41;

                      

                       A234: (o,b1) // (o,b) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                      then (o,b) // (o,c1) by A74, A233, AFF_1: 5;

                      then (o,b) // (o,c) by A222, A232, AFF_1: 5;

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

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

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

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

                      then (b,c) // (o,b1) by A29, A234, AFF_1: 5;

                      then

                       A235: (b,c) // (b1,o) by AFF_1: 4;

                       LIN (o,b1,c1) by A233, AFF_1:def 1;

                      then LIN (b1,c1,o) by AFF_1: 6;

                      then (b1,c1) // (b1,o) by AFF_1:def 1;

                      hence contradiction by A47, A74, A235, AFF_1: 5;

                    end;

                     A236:

                    now

                      

                       A237: d <> d1

                      proof

                        assume d = d1;

                        then

                         A238: (o,a) // (a,d) by A85, A86, A87, A109, AFF_1: 39, AFF_1: 41;

                        (o,a) // (a,a1) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                        then (a,a1) // (a,d) by A28, A238, AFF_1: 5;

                        hence contradiction by A46, AFF_1:def 1;

                      end;

                      assume

                       A239: d1 in K;

                      (c,c1) // (c,o) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                      then

                       A240: LIN (c,c1,o) by AFF_1:def 1;

                      

                       A241: (d,d1) // (c1,c) by A110, AFF_1: 4;

                      d in K by A45, A159, A153, A154, A155, AFF_1: 25;

                      then c in K by A153, A155, A239, A237, A241, AFF_1: 48;

                      hence contradiction by A48, A153, A155, A221, A240, AFF_1: 25;

                    end;

                     A242:

                    now

                      assume a1 in K;

                      then

                       A243: (a1,b1) // (a1,c1) by A153, A154, A155, AFF_1: 39, AFF_1: 41;

                      then (a,b) // (a1,c1) by A42, A75, AFF_1: 5;

                      then (a,b) // (a,c) by A43, A75, AFF_1: 5;

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

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

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

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

                      then

                       A244: (b,c) // (a1,b1) by A42, A215, AFF_1: 5;

                       LIN (a1,b1,c1) by A243, AFF_1:def 1;

                      then LIN (b1,c1,a1) by AFF_1: 6;

                      then (b1,c1) // (b1,a1) by AFF_1:def 1;

                      then (b1,c1) // (a1,b1) by AFF_1: 4;

                      hence contradiction by A47, A75, A244, AFF_1: 5;

                    end;

                     A245:

                    now

                      

                       A246: d <> d2

                      proof

                        assume d = d2;

                        then

                         A247: (o,a) // (a,d) by A85, A86, A87, A107, AFF_1: 39, AFF_1: 41;

                        (o,a) // (a,a1) by A25, A31, A32, A37, AFF_1: 39, AFF_1: 41;

                        then (a,a1) // (a,d) by A28, A247, AFF_1: 5;

                        hence contradiction by A46, AFF_1:def 1;

                      end;

                      assume

                       A248: d2 in K;

                      (d,d2) // (a1,c1) by A43, A215, A108, AFF_1: 5;

                      then

                       A249: (d,d2) // (c1,a1) by AFF_1: 4;

                      d in K by A45, A159, A153, A154, A155, AFF_1: 25;

                      hence contradiction by A153, A155, A242, A248, A246, A249, AFF_1: 48;

                    end;

                    assume not thesis;

                    hence contradiction by A221, A242, A236, A245;

                  end;

                  

                   A250: not c1 in C & not b1 in C & not d in C & not d4 in C

                  proof

                     A251:

                    now

                      assume

                       A252: c1 in C;

                      (o,c1) // (c1,c) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                      hence contradiction by A155, A85, A86, A187, A220, A252, AFF_1: 48;

                    end;

                     A253:

                    now

                      assume

                       A254: d4 in C;

                      (d1,d4) // (d1,d3) by A186, AFF_1: 4;

                      hence contradiction by A85, A109, A185, A187, A220, A254, AFF_1: 48;

                    end;

                     A255:

                    now

                      assume

                       A256: b1 in C;

                      (o,b1) // (o,b) by A26, A33, A34, A38, AFF_1: 39, AFF_1: 41;

                      hence contradiction by A74, A85, A86, A187, A256, AFF_1: 48;

                    end;

                    assume not thesis;

                    hence contradiction by A187, A251, A255, A253;

                  end;

                  a <> c

                  proof

                    assume a = c;

                    then

                     A257: (o,a) // M by A27, A35, A39, AFF_1: 52;

                    (o,a) // Y by A25, A31, A37, AFF_1: 52;

                    hence contradiction by A25, A27, A28, A41, A257, AFF_1: 45, AFF_1: 53;

                  end;

                  then (a1,c1) // (d,d2) by A43, A108, AFF_1: 5;

                  then

                   A258: (a1,c1) // (d2,d) by AFF_1: 4;

                  (c1,o) // (c,c1) by A27, A35, A36, A39, AFF_1: 39, AFF_1: 41;

                  then

                   A259: (c1,o) // (d,d1) by A48, A110, AFF_1: 5;

                  

                   A260: d1 <> d2

                  proof

                    assume d1 = d2;

                    then (a,c) // (c,c1) by A109, A110, A108, A187, AFF_1: 5;

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

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

                    then a in M by A35, A36, A39, A48, AFF_1: 25;

                    then

                     A261: (o,a) // M by A27, A39, AFF_1: 52;

                    (o,a) // Y by A25, A31, A37, AFF_1: 52;

                    hence contradiction by A25, A27, A28, A41, A261, AFF_1: 45, AFF_1: 53;

                  end;

                  

                   A262: not LIN (d4,d2,d1)

                  proof

                    assume LIN (d4,d2,d1);

                    then LIN (d1,d2,d4) by AFF_1: 6;

                    hence contradiction by A85, A109, A107, A250, A260, AFF_1: 25;

                  end;

                  

                   A263: (o,b) // (o,b1) by A26, A33, A34, A38, AFF_1: 51;

                  (a,c) // (d2,d) by A108, AFF_1: 4;

                  then (a,b) // (d2,d3) by A24, A113, A114, A115, A85, A86, A87, A109, A107, A157, A158, A116, A129, A187, A111;

                  then

                   A264: (d2,d3) // (a1,b1) by A42, A215, AFF_1: 5;

                  (o,b) // (d1,d4) by A109, A158, A186, A187, AFF_1: 5;

                  then (o,b1) // (d1,d4) by A29, A263, AFF_1: 5;

                  then (a1,b1) // (d2,d4) by A24, A153, A154, A155, A85, A86, A109, A107, A185, A112, A156, A220, A250, A258, A259;

                  then (d2,d3) // (d2,d4) by A75, A264, AFF_1: 5;

                  then LIN (d2,d3,d4) by AFF_1:def 1;

                  then LIN (d4,d3,d2) by AFF_1: 6;

                  then

                   A265: (d4,d3) // (d4,d2) by AFF_1:def 1;

                   LIN (d1,d3,d4) by A186, AFF_1:def 1;

                  then LIN (d4,d3,d1) by AFF_1: 6;

                  then (d4,d3) // (d4,d1) by AFF_1:def 1;

                  then (d4,d2) // (d4,d1) by A206, A265, AFF_1: 5;

                  hence contradiction by A262, AFF_1:def 1;

                end;

                now

                  assume

                   A266: b1 = o;

                  

                   A267: o = a1

                  proof

                    

                     A268: not LIN (b,a,o)

                    proof

                      assume LIN (b,a,o);

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

                      then b in Y by A25, A28, A31, A37, AFF_1: 25;

                      then

                       A269: (o,b) // Y by A25, A37, AFF_1: 52;

                      (o,b) // Z by A26, A33, A38, AFF_1: 52;

                      hence contradiction by A25, A26, A29, A40, A269, AFF_1: 45, AFF_1: 53;

                    end;

                    

                     A270: a1 <> a

                    proof

                      assume a1 = a;

                      then LIN (a,b,o) by A42, A266, AFF_1:def 1;

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

                      then b in Y by A25, A28, A31, A37, AFF_1: 25;

                      then

                       A271: (o,b) // Y by A25, A37, AFF_1: 52;

                      (o,b) // Z by A26, A33, A38, AFF_1: 52;

                      hence contradiction by A25, A26, A29, A40, A271, AFF_1: 45, AFF_1: 53;

                    end;

                    assume

                     A272: o <> a1;

                    (a1,o) // (a,a1) by A25, A31, A32, A37, AFF_1: 51;

                    then (a,b) // (a,a1) by A42, A266, A272, AFF_1: 5;

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

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

                    then

                     A273: (a1,b) // (a1,a) by AFF_1:def 1;

                    (a1,a) // (a1,o) by A25, A31, A32, A37, AFF_1: 51;

                    then (a1,b) // (a1,o) by A273, A270, AFF_1: 5;

                    then LIN (a1,b,o) by AFF_1:def 1;

                    then LIN (b,o,a1) by AFF_1: 6;

                    hence contradiction by A25, A31, A32, A37, A272, A268, AFF_1: 14, AFF_1: 51;

                  end;

                  o = c1

                  proof

                    

                     A274: not LIN (a,c,o)

                    proof

                      assume LIN (a,c,o);

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

                      then c in Y by A25, A28, A31, A37, AFF_1: 25;

                      then

                       A275: (o,c) // Y by A25, A37, AFF_1: 52;

                      (o,c) // M by A27, A35, A39, AFF_1: 52;

                      hence contradiction by A25, A27, A30, A41, A275, AFF_1: 45, AFF_1: 53;

                    end;

                    assume

                     A276: o <> c1;

                    

                     A277: (o,c1) // (o,c) by A27, A35, A36, A39, AFF_1: 51;

                    then (o,c) // (a,c) by A43, A267, A276, AFF_1: 5;

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

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

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

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

                    then (o,a) // (o,c1) by A30, A277, AFF_1: 5;

                    then LIN (o,a,c1) by AFF_1:def 1;

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

                    hence contradiction by A27, A35, A36, A39, A276, A274, AFF_1: 14, AFF_1: 51;

                  end;

                  hence contradiction by A47, A266, AFF_1: 3;

                end;

                hence contradiction by A73;

              end;

              hence contradiction by A47, AFF_1: 3;

            end;

            hence LIN (a,a1,d) or (b,c) // (b1,c1);

          end;

           A278:

          now

            

             A279: M // M by A17, AFF_1: 41;

            consider d such that

             A280: LIN (b,c,d) and

             A281: LIN (b1,c1,d) by A22, AFF_1: 60;

            

             A282: LIN (a,a1,d) by A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23, A280, A281;

            

             A283: not a in Z & not a in M

            proof

               A284:

              now

                assume a in M;

                then

                 A285: (o,a) // M by A5, A17, AFF_1: 52;

                (o,a) // Y by A3, A9, A15, AFF_1: 52;

                hence contradiction by A3, A5, A6, A19, A285, AFF_1: 45, AFF_1: 53;

              end;

               A286:

              now

                assume a in Z;

                then

                 A287: (o,a) // Z by A4, A16, AFF_1: 52;

                (o,a) // Y by A3, A9, A15, AFF_1: 52;

                hence contradiction by A3, A4, A6, A18, A287, AFF_1: 45, AFF_1: 53;

              end;

              assume not thesis;

              hence contradiction by A286, A284;

            end;

            

             A288: ex d1 st (a,b) // (d,d1) & d1 in Z

            proof

              consider e1 such that

               A289: (o,b) // (o,e1) and

               A290: o <> e1 by DIRAF: 40;

              consider e2 such that

               A291: (a,b) // (d,e2) and

               A292: d <> e2 by DIRAF: 40;

               not (o,e1) // (d,e2)

              proof

                assume (o,e1) // (d,e2);

                then (o,b) // (d,e2) by A289, A290, AFF_1: 5;

                then (o,b) // (a,b) by A291, A292, AFF_1: 5;

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

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

                hence contradiction by A4, A7, A11, A16, A283, AFF_1: 25;

              end;

              then

              consider d1 such that

               A293: LIN (o,e1,d1) and

               A294: LIN (d,e2,d1) by AFF_1: 60;

              (o,e1) // (o,d1) by A293, AFF_1:def 1;

              then (o,b) // (o,d1) by A289, A290, AFF_1: 5;

              then

               A295: LIN (o,b,d1) by AFF_1:def 1;

              take d1;

              (d,e2) // (d,d1) by A294, AFF_1:def 1;

              hence thesis by A4, A7, A11, A16, A291, A292, A295, AFF_1: 5, AFF_1: 25;

            end;

            

             A296: Z // Z by A16, AFF_1: 41;

            

             A297: a <> a1 & b <> b1 & c <> c1

            proof

               A298:

              now

                

                 A299: not LIN (a,o,b)

                proof

                  assume LIN (a,o,b);

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

                  hence contradiction by A4, A7, A11, A16, A283, AFF_1: 25;

                end;

                

                 A300: not LIN (a,o,c)

                proof

                  assume LIN (a,o,c);

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

                  hence contradiction by A5, A8, A13, A17, A283, AFF_1: 25;

                end;

                assume

                 A301: a = a1;

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

                then

                 A302: c = c1 by A5, A13, A14, A279, A300, AFF_1: 14, AFF_1: 39;

                 LIN (a,b,b1) by A20, A301, AFF_1:def 1;

                then b = b1 by A4, A11, A12, A296, A299, AFF_1: 14, AFF_1: 39;

                hence contradiction by A22, A302, AFF_1: 2;

              end;

               A303:

              now

                assume b = b1;

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

                then

                 A304: LIN (b,a,a1) by AFF_1:def 1;

                (o,a) // (o,a1) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

                hence contradiction by A4, A7, A11, A16, A283, A298, A304, AFF_1: 14, AFF_1: 25;

              end;

               A305:

              now

                assume c = c1;

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

                then

                 A306: LIN (c,a,a1) by AFF_1:def 1;

                (o,a) // (o,a1) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

                hence contradiction by A5, A8, A13, A17, A283, A298, A306, AFF_1: 14, AFF_1: 25;

              end;

              assume not thesis;

              hence contradiction by A298, A303, A305;

            end;

            

             A307: a1 <> o & b1 <> o & c1 <> o

            proof

               A308:

              now

                assume

                 A309: a1 = o;

                

                 A310: o = c1

                proof

                  

                   A311: not LIN (c,a,o)

                  proof

                    assume LIN (c,a,o);

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

                    hence contradiction by A5, A8, A13, A17, A283, AFF_1: 25;

                  end;

                  assume

                   A312: o <> c1;

                  

                   A313: (o,c1) // (o,c) by A5, A13, A14, A17, AFF_1: 39, AFF_1: 41;

                  then (a,c) // (o,c) by A21, A309, A312, AFF_1: 5;

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

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

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

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

                  then (o,c1) // (o,a) by A8, A313, AFF_1: 5;

                  then LIN (o,c1,a) by AFF_1:def 1;

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

                  then

                   A314: (a,o) // (a,c1) by AFF_1:def 1;

                  (c,o) // (c,c1) by A5, A13, A14, A17, AFF_1: 39, AFF_1: 41;

                  then LIN (c,o,c1) by AFF_1:def 1;

                  hence contradiction by A312, A311, A314, AFF_1: 14;

                end;

                o = b1

                proof

                  

                   A315: not LIN (b,a,o)

                  proof

                    assume LIN (b,a,o);

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

                    hence contradiction by A4, A7, A11, A16, A283, AFF_1: 25;

                  end;

                  assume

                   A316: o <> b1;

                  

                   A317: (o,b1) // (o,b) by A4, A11, A12, A16, AFF_1: 39, AFF_1: 41;

                  then (a,b) // (o,b) by A20, A309, A316, AFF_1: 5;

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

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

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

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

                  then (o,a) // (o,b1) by A7, A317, AFF_1: 5;

                  then LIN (o,a,b1) by AFF_1:def 1;

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

                  then

                   A318: (a,o) // (a,b1) by AFF_1:def 1;

                  (b,o) // (b,b1) by A4, A11, A12, A16, AFF_1: 39, AFF_1: 41;

                  then LIN (b,o,b1) by AFF_1:def 1;

                  hence contradiction by A316, A315, A318, AFF_1: 14;

                end;

                hence contradiction by A22, A310, AFF_1: 3;

              end;

               A319:

              now

                

                 A320: not LIN (a,b,o)

                proof

                  assume LIN (a,b,o);

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

                  hence contradiction by A4, A7, A11, A16, A283, AFF_1: 25;

                end;

                

                 A321: (a1,o) // (a,a1) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

                assume b1 = o;

                then (a,b) // (a,a1) by A20, A308, A321, AFF_1: 5;

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

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

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

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

                then (a1,b) // (a1,o) by A297, A321, AFF_1: 5;

                then LIN (a1,b,o) by AFF_1:def 1;

                then LIN (b,o,a1) by AFF_1: 6;

                then

                 A322: (b,o) // (b,a1) by AFF_1:def 1;

                (a,o) // (a,a1) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

                then LIN (a,o,a1) by AFF_1:def 1;

                hence contradiction by A308, A320, A322, AFF_1: 14;

              end;

               A323:

              now

                

                 A324: not LIN (a,c,o)

                proof

                  assume LIN (a,c,o);

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

                  hence contradiction by A5, A8, A13, A17, A283, AFF_1: 25;

                end;

                

                 A325: (a1,o) // (a,a1) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

                assume c1 = o;

                then (a,c) // (a,a1) by A21, A308, A325, AFF_1: 5;

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

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

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

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

                then (a1,o) // (a1,c) by A297, A325, AFF_1: 5;

                then LIN (a1,o,c) by AFF_1:def 1;

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

                then

                 A326: (c,o) // (c,a1) by AFF_1:def 1;

                (a,o) // (a,a1) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

                then LIN (a,o,a1) by AFF_1:def 1;

                hence contradiction by A308, A324, A326, AFF_1: 14;

              end;

              assume not thesis;

              hence contradiction by A308, A319, A323;

            end;

            ex d2 st (a,c) // (d,d2) & d2 in M

            proof

              consider e1 such that

               A327: (o,c) // (o,e1) and

               A328: o <> e1 by DIRAF: 40;

              consider e2 such that

               A329: (a,c) // (d,e2) and

               A330: d <> e2 by DIRAF: 40;

               not (o,e1) // (d,e2)

              proof

                assume (o,e1) // (d,e2);

                then (o,c) // (d,e2) by A327, A328, AFF_1: 5;

                then (o,c) // (a,c) by A329, A330, AFF_1: 5;

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

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

                hence contradiction by A5, A8, A13, A17, A283, AFF_1: 25;

              end;

              then

              consider d2 such that

               A331: LIN (o,e1,d2) and

               A332: LIN (d,e2,d2) by AFF_1: 60;

              (o,e1) // (o,d2) by A331, AFF_1:def 1;

              then (o,c) // (o,d2) by A327, A328, AFF_1: 5;

              then

               A333: LIN (o,c,d2) by AFF_1:def 1;

              take d2;

              (d,e2) // (d,d2) by A332, AFF_1:def 1;

              hence thesis by A5, A8, A13, A17, A329, A330, A333, AFF_1: 5, AFF_1: 25;

            end;

            then

            consider d2 such that

             A334: (a,c) // (d,d2) and

             A335: d2 in M;

            consider d1 such that

             A336: (a,b) // (d,d1) and

             A337: d1 in Z by A288;

            assume

             A338: not Z // M;

            

             A339: d1 <> d2

            proof

              

               A340: o <> d1

              proof

                

                 A341: o <> d

                proof

                  assume o = d;

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

                  then c in Z by A4, A7, A11, A16, AFF_1: 25;

                  then

                   A342: (o,c) // Z by A4, A16, AFF_1: 52;

                  (o,c) // M by A5, A13, A17, AFF_1: 52;

                  hence contradiction by A8, A338, A342, AFF_1: 53;

                end;

                

                 A343: (a,a1) // (a,d) by A282, AFF_1:def 1;

                (a,o) // (a,a1) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

                then (a,o) // (a,d) by A297, A343, AFF_1: 5;

                then LIN (a,o,d) by AFF_1:def 1;

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

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

                then

                 A344: (a,o) // (d,o) by AFF_1: 4;

                assume o = d1;

                then (a,b) // (a,o) by A336, A341, A344, AFF_1: 5;

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

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

                hence contradiction by A4, A7, A11, A16, A283, AFF_1: 25;

              end;

              assume d1 = d2;

              then

               A345: (o,d1) // M by A5, A17, A335, AFF_1: 52;

              (o,d1) // Z by A4, A16, A337, AFF_1: 52;

              hence contradiction by A338, A345, A340, AFF_1: 53;

            end;

             A346:

            now

              assume

               A347: (b1,c1) // (d1,d2);

              ex d5 st LIN (b,c,d5) & LIN (d1,d2,d5)

              proof

                consider e1 such that

                 A348: (b,c) // (b,e1) and

                 A349: b <> e1 by DIRAF: 40;

                consider e2 such that

                 A350: (d1,d2) // (d1,e2) and

                 A351: d1 <> e2 by DIRAF: 40;

                 not (b,e1) // (d1,e2)

                proof

                  assume (b,e1) // (d1,e2);

                  then (b,e1) // (d1,d2) by A350, A351, AFF_1: 5;

                  then (b,c) // (d1,d2) by A348, A349, AFF_1: 5;

                  hence contradiction by A22, A339, A347, AFF_1: 5;

                end;

                then

                consider d5 such that

                 A352: LIN (b,e1,d5) and

                 A353: LIN (d1,e2,d5) by AFF_1: 60;

                (b,e1) // (b,d5) by A352, AFF_1:def 1;

                then

                 A354: (b,c) // (b,d5) by A348, A349, AFF_1: 5;

                take d5;

                (d1,e2) // (d1,d5) by A353, AFF_1:def 1;

                then (d1,d2) // (d1,d5) by A350, A351, AFF_1: 5;

                hence thesis by A354, AFF_1:def 1;

              end;

              then

              consider d5 such that

               A355: LIN (b,c,d5) and

               A356: LIN (d1,d2,d5);

              

               A357: d in Y by A9, A10, A15, A297, A282, AFF_1: 25;

               A358:

              now

                

                 A359: not LIN (a,b,d)

                proof

                  

                   A360: a <> d

                  proof

                    

                     A361: a1 <> b1

                    proof

                      (o,a1) // (o,a) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

                      then

                       A362: LIN (o,a1,a) by AFF_1:def 1;

                      assume a1 = b1;

                      hence contradiction by A4, A12, A16, A283, A307, A362, AFF_1: 25;

                    end;

                    assume

                     A363: a = d;

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

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

                    then (a1,b1) // (a,c) by A11, A20, A283, AFF_1: 5;

                    then (a1,b1) // (a1,c1) by A13, A21, A283, AFF_1: 5;

                    then LIN (a1,b1,c1) by AFF_1:def 1;

                    then LIN (b1,c1,a1) by AFF_1: 6;

                    then (b1,c1) // (b1,a1) by AFF_1:def 1;

                    then

                     A364: (b1,c1) // (a1,b1) by AFF_1: 4;

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

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

                    then (b,c) // (a1,b1) by A11, A20, A283, AFF_1: 5;

                    hence contradiction by A22, A364, A361, AFF_1: 5;

                  end;

                  assume LIN (a,b,d);

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

                  then b in Y by A9, A15, A357, A360, AFF_1: 25;

                  then

                   A365: (o,b) // Y by A3, A15, AFF_1: 52;

                  (o,b) // Z by A4, A11, A16, AFF_1: 52;

                  hence contradiction by A3, A4, A7, A18, A365, AFF_1: 45, AFF_1: 53;

                end;

                assume

                 A366: LIN (a,d,d5);

                

                 A367: o <> d

                proof

                  

                   A368: (o,b) // (o,b1) by A4, A11, A12, A16, AFF_1: 39, AFF_1: 41;

                  assume

                   A369: o = d;

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

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

                  then

                   A370: (o,b1) // (o,c) by A7, A368, AFF_1: 5;

                  (o,c) // (o,c1) by A5, A13, A14, A17, AFF_1: 39, AFF_1: 41;

                  then (o,b1) // (o,c1) by A8, A370, AFF_1: 5;

                  then LIN (o,b1,c1) by AFF_1:def 1;

                  then LIN (b1,c1,o) by AFF_1: 6;

                  then (b1,c1) // (b1,o) by AFF_1:def 1;

                  then

                   A371: (b1,c1) // (o,b1) by AFF_1: 4;

                  (b,c) // (b,o) by A280, A369, AFF_1:def 1;

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

                  then (b,c) // (o,b1) by A7, A368, AFF_1: 5;

                  hence contradiction by A22, A307, A371, AFF_1: 5;

                end;

                

                 A372: d <> d1

                proof

                  assume d = d1;

                  then

                   A373: (o,d) // Z by A4, A16, A337, AFF_1: 52;

                  (o,d) // Y by A3, A15, A357, AFF_1: 52;

                  hence contradiction by A3, A4, A18, A367, A373, AFF_1: 45, AFF_1: 53;

                end;

                

                 A374: d <> d2

                proof

                  assume d = d2;

                  then

                   A375: (o,d) // M by A5, A17, A335, AFF_1: 52;

                  (o,d) // Y by A3, A15, A357, AFF_1: 52;

                  hence contradiction by A3, A5, A19, A367, A375, AFF_1: 45, AFF_1: 53;

                end;

                

                 A376: (b,c) // (b,d5) by A355, AFF_1:def 1;

                

                 A377: (b,c) // (b,d) by A280, AFF_1:def 1;

                b <> c by A22, AFF_1: 3;

                then (b,d) // (b,d5) by A377, A376, AFF_1: 5;

                then LIN (d1,d2,d) by A356, A366, A359, AFF_1: 14;

                then LIN (d,d1,d2) by AFF_1: 6;

                then (d,d1) // (d,d2) by AFF_1:def 1;

                then (a,b) // (d,d2) by A336, A372, AFF_1: 5;

                then

                 A378: (a,b) // (a,c) by A334, A374, AFF_1: 5;

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

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

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

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

                then

                 A379: (b,c) // (a1,b1) by A11, A20, A283, AFF_1: 5;

                (a1,b1) // (a,c) by A11, A20, A283, A378, AFF_1: 5;

                then (a1,b1) // (a1,c1) by A13, A21, A283, AFF_1: 5;

                then LIN (a1,b1,c1) by AFF_1:def 1;

                then LIN (b1,c1,a1) by AFF_1: 6;

                then (b1,c1) // (b1,a1) by AFF_1:def 1;

                then

                 A380: (b1,c1) // (a1,b1) by AFF_1: 4;

                a1 <> b1

                proof

                  (o,a1) // (o,a) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

                  then

                   A381: LIN (o,a1,a) by AFF_1:def 1;

                  assume a1 = b1;

                  hence contradiction by A4, A12, A16, A283, A307, A381, AFF_1: 25;

                end;

                hence contradiction by A22, A380, A379, AFF_1: 5;

              end;

               not (b,c) // (d1,d2) by A22, A339, A347, AFF_1: 5;

              hence contradiction by A2, A3, A4, A5, A6, A7, A8, A9, A11, A13, A15, A16, A17, A18, A19, A23, A336, A337, A334, A335, A355, A356, A357, A358;

            end;

            now

              

               A382: d in Y by A9, A10, A15, A297, A282, AFF_1: 25;

              

               A383: not LIN (a1,b1,d)

              proof

                

                 A384: a1 <> d

                proof

                  

                   A385: a1 <> b1 & a1 <> c1

                  proof

                    (o,a1) // (o,a) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

                    then

                     A386: LIN (o,a1,a) by AFF_1:def 1;

                    assume not thesis;

                    hence contradiction by A4, A5, A12, A14, A16, A17, A283, A307, A386, AFF_1: 25;

                  end;

                  assume

                   A387: a1 = d;

                  then LIN (a1,b1,c1) by A281, AFF_1: 6;

                  then (a1,b1) // (a1,c1) by AFF_1:def 1;

                  then (a,b) // (a1,c1) by A20, A385, AFF_1: 5;

                  then (a,b) // (a,c) by A21, A385, AFF_1: 5;

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

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

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

                  then

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

                  (b1,c1) // (b1,a1) by A281, A387, AFF_1:def 1;

                  then (b1,c1) // (a1,b1) by AFF_1: 4;

                  then (b1,c1) // (a,b) by A20, A385, AFF_1: 5;

                  hence contradiction by A11, A22, A283, A388, AFF_1: 5;

                end;

                assume LIN (a1,b1,d);

                then LIN (a1,d,b1) by AFF_1: 6;

                then b1 in Y by A10, A15, A382, A384, AFF_1: 25;

                then (o,b1) // (o,a) by A3, A9, A15, AFF_1: 39, AFF_1: 41;

                then LIN (o,b1,a) by AFF_1:def 1;

                hence contradiction by A4, A12, A16, A283, A307, AFF_1: 25;

              end;

              

               A389: d <> o

              proof

                

                 A390: (o,b) // (o,b1) by A4, A11, A12, A16, AFF_1: 39, AFF_1: 41;

                assume

                 A391: d = o;

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

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

                then

                 A392: (o,b1) // (o,c) by A7, A390, AFF_1: 5;

                (o,c) // (o,c1) by A5, A13, A14, A17, AFF_1: 39, AFF_1: 41;

                then (o,b1) // (o,c1) by A8, A392, AFF_1: 5;

                then LIN (o,b1,c1) by AFF_1:def 1;

                then LIN (b1,c1,o) by AFF_1: 6;

                then (b1,c1) // (b1,o) by AFF_1:def 1;

                then

                 A393: (b1,c1) // (o,b1) by AFF_1: 4;

                (b,c) // (b,o) by A280, A391, AFF_1:def 1;

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

                then (b,c) // (o,b1) by A7, A390, AFF_1: 5;

                hence contradiction by A22, A307, A393, AFF_1: 5;

              end;

              

               A394: d <> d1

              proof

                (o,d) // (o,a) by A3, A9, A15, A382, AFF_1: 39, AFF_1: 41;

                then

                 A395: LIN (o,d,a) by AFF_1:def 1;

                assume d = d1;

                hence contradiction by A4, A16, A283, A337, A389, A395, AFF_1: 25;

              end;

              

               A396: d <> d2

              proof

                (o,d) // (o,a) by A3, A9, A15, A382, AFF_1: 39, AFF_1: 41;

                then

                 A397: LIN (o,d,a) by AFF_1:def 1;

                assume d = d2;

                hence contradiction by A5, A17, A283, A335, A389, A397, AFF_1: 25;

              end;

              

               A398: (a1,c1) // (d,d2) by A13, A21, A283, A334, AFF_1: 5;

              

               A399: b1 <> c1 by A22, AFF_1: 3;

              

               A400: (b1,c1) // (b1,d) by A281, AFF_1:def 1;

              assume

               A401: not (b1,c1) // (d1,d2);

              then

              consider d5 such that

               A402: LIN (b1,c1,d5) and

               A403: LIN (d1,d2,d5) by AFF_1: 60;

              (b1,c1) // (b1,d5) by A402, AFF_1:def 1;

              then

               A404: (b1,d) // (b1,d5) by A399, A400, AFF_1: 5;

              (a1,b1) // (d,d1) by A11, A20, A283, A336, AFF_1: 5;

              then LIN (a1,d,d5) by A2, A3, A4, A5, A10, A12, A14, A15, A16, A17, A18, A19, A23, A307, A337, A335, A401, A402, A403, A382, A398;

              then d = d5 by A383, A404, AFF_1: 14;

              then LIN (d,d1,d2) by A403, AFF_1: 6;

              then (d,d1) // (d,d2) by AFF_1:def 1;

              then (a,b) // (d,d2) by A336, A394, AFF_1: 5;

              then

               A405: (a,b) // (a,c) by A334, A396, AFF_1: 5;

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

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

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

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

              then

               A406: (b,c) // (a1,b1) by A11, A20, A283, AFF_1: 5;

              (a1,b1) // (a,c) by A11, A20, A283, A405, AFF_1: 5;

              then (a1,b1) // (a1,c1) by A13, A21, A283, AFF_1: 5;

              then LIN (a1,b1,c1) by AFF_1:def 1;

              then LIN (b1,c1,a1) by AFF_1: 6;

              then (b1,c1) // (b1,a1) by AFF_1:def 1;

              then

               A407: (b1,c1) // (a1,b1) by AFF_1: 4;

              a1 <> b1

              proof

                (o,a1) // (o,a) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

                then

                 A408: LIN (o,a1,a) by AFF_1:def 1;

                assume a1 = b1;

                hence contradiction by A4, A12, A16, A283, A307, A408, AFF_1: 25;

              end;

              hence contradiction by A22, A407, A406, AFF_1: 5;

            end;

            hence contradiction by A346;

          end;

          now

            assume

             A409: Z // M;

            then

             A410: b1 in M by A4, A5, A12, AFF_1: 45;

            b in M by A4, A5, A11, A409, AFF_1: 45;

            hence contradiction by A13, A14, A17, A22, A410, AFF_1: 39, AFF_1: 41;

          end;

          hence contradiction by A278;

        end;

        hence thesis by AFF_2:def 4;

      end;

      X is Desarguesian implies X is satisfying_Scherungssatz

      proof

        assume

         A411: X is Desarguesian;

        then X is satisfying_TDES_1 by AFF_2: 3, AFF_2: 12;

        then X is satisfying_des_1 by AFF_2: 13;

        then X is translational by AFF_2: 7;

        then

         A412: X is satisfying_minor_Scherungssatz by Th6;

        X is satisfying_major_Scherungssatz by A411, Th7;

        hence thesis by A412, Th2;

      end;

      hence thesis by A1;

    end;

    theorem :: CONMETR1:9

    

     Th9: X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz

    proof

      

       A1: X is satisfying_minor_indirect_Scherungssatz implies X is satisfying_pap

      proof

        assume

         A2: X is satisfying_minor_indirect_Scherungssatz;

        now

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

          assume that M is being_line and N is being_line and

           A3: a in M and

           A4: b in M and

           A5: c in M and

           A6: M // N and

           A7: M <> N and

           A8: a1 in N and

           A9: b1 in N and

           A10: c1 in N and

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

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

          

           A13: not b in N by A4, A6, A7, AFF_1: 45;

          

           A14: not c1 in M by A6, A7, A10, AFF_1: 45;

          

           A15: not c in N by A5, A6, A7, AFF_1: 45;

          

           A16: (b1,b) // (b,b1) by AFF_1: 2;

          

           A17: not b1 in M by A6, A7, A9, AFF_1: 45;

          

           A18: (b,c1) // (b1,c) by A12, AFF_1: 4;

          

           A19: not a1 in M by A6, A7, A8, AFF_1: 45;

          

           A20: (a,b1) // (a1,b) by A11, AFF_1: 4;

           not a in N by A3, A6, A7, AFF_1: 45;

          then (a,c1) // (a1,c) by A2, A3, A4, A5, A6, A8, A9, A10, A13, A15, A19, A17, A14, A20, A18, A16;

          hence (a,c1) // (c,a1) by AFF_1: 4;

        end;

        hence thesis by AFF_2:def 13;

      end;

      X is satisfying_pap implies X is satisfying_minor_indirect_Scherungssatz

      proof

        assume

         A21: X is satisfying_pap;

        now

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

          assume that

           A22: M // N and

           A23: a1 in M and

           A24: a3 in M and

           A25: b2 in M and

           A26: b4 in M and

           A27: a2 in N and

           A28: a4 in N and

           A29: b1 in N and

           A30: b3 in N and

           A31: not a4 in M and not a2 in M and not b1 in M and not b3 in M and not a1 in N and not a3 in N and not b2 in N and not b4 in N and

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

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

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

          

           A35: M is being_line by A22, AFF_1: 36;

          

           A36: (b2,b3) // (a3,a2) by A32, AFF_1: 4;

          

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

          

           A38: (a4,a1) // (b1,b4) by A34, AFF_1: 4;

          (a1,a2) // (b2,b1) by A33, AFF_1: 4;

          then (a1,b3) // (a3,b1) by A21, A22, A23, A24, A25, A27, A28, A29, A30, A31, A35, A37, A36, AFF_2:def 13;

          then (b1,a3) // (b3,a1) by AFF_1: 4;

          then (a4,a3) // (b3,b4) by A21, A22, A23, A24, A26, A28, A29, A30, A31, A35, A37, A38, AFF_2:def 13;

          hence (a3,a4) // (b3,b4) by AFF_1: 4;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: CONMETR1:10

    

     Th10: X is Pappian iff X is satisfying_major_indirect_Scherungssatz

    proof

      

       A1: X is Pappian implies X is satisfying_major_indirect_Scherungssatz

      proof

        assume

         A2: X is Pappian;

        then

         A3: X is Desarguesian by AFF_2: 11;

        now

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

          assume that

           A4: M is being_line and

           A5: N is being_line and

           A6: o in M and

           A7: o in N and

           A8: a1 in M and

           A9: a3 in M and

           A10: b2 in M and

           A11: b4 in M and

           A12: a2 in N and

           A13: a4 in N and

           A14: b1 in N and

           A15: b3 in N and

           A16: not a4 in M and

           A17: not a2 in M and

           A18: not b1 in M and

           A19: not b3 in M and

           A20: not a1 in N and

           A21: not a3 in N and

           A22: not b2 in N and

           A23: not b4 in N and

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

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

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

           A27:

          now

            assume that

             A28: a1 <> a3 and

             A29: a2 <> a4;

            ex x, y, z st LIN (x,y,z) & x <> y & x <> z & y <> z

            proof

              (o,a1) // (o,a3) by A4, A6, A8, A9, AFF_1: 39, AFF_1: 41;

              then

               A30: LIN (o,a1,a3) by AFF_1:def 1;

              assume not thesis;

              hence contradiction by A7, A20, A21, A28, A30;

            end;

            then

            consider d such that

             A31: LIN (a2,a1,d) and

             A32: a2 <> d and

             A33: a1 <> d by TRANSLAC: 1;

            

             A34: (a2,a1) // (a2,d) by A31, AFF_1:def 1;

            

             A35: ex c2 st c2 in M & (a2,a3) // (b1,c2)

            proof

              consider e2 such that

               A36: (a1,a3) // (a1,e2) and

               A37: a1 <> e2 by DIRAF: 40;

              consider e1 such that

               A38: (a2,a3) // (b1,e1) and

               A39: b1 <> e1 by DIRAF: 40;

               not (b1,e1) // (a1,e2)

              proof

                assume (b1,e1) // (a1,e2);

                then (a2,a3) // (a1,e2) by A38, A39, AFF_1: 5;

                then (a2,a3) // (a1,a3) by A36, A37, AFF_1: 5;

                then (a3,a1) // (a3,a2) by AFF_1: 4;

                then LIN (a3,a1,a2) by AFF_1:def 1;

                hence contradiction by A4, A8, A9, A17, A28, AFF_1: 25;

              end;

              then

              consider c2 such that

               A40: LIN (b1,e1,c2) and

               A41: LIN (a1,e2,c2) by AFF_1: 60;

              (a1,e2) // (a1,c2) by A41, AFF_1:def 1;

              then (a1,a3) // (a1,c2) by A36, A37, AFF_1: 5;

              then

               A42: LIN (a1,a3,c2) by AFF_1:def 1;

              take c2;

              (b1,e1) // (b1,c2) by A40, AFF_1:def 1;

              hence thesis by A4, A8, A9, A28, A38, A39, A42, AFF_1: 5, AFF_1: 25;

            end;

            

             A43: ex c1 st c1 in N & (a1,a4) // (b2,c1)

            proof

              consider e2 such that

               A44: (a2,a4) // (a2,e2) and

               A45: a2 <> e2 by DIRAF: 40;

              consider e1 such that

               A46: (a1,a4) // (b2,e1) and

               A47: b2 <> e1 by DIRAF: 40;

               not (b2,e1) // (a2,e2)

              proof

                assume (b2,e1) // (a2,e2);

                then (a1,a4) // (a2,e2) by A46, A47, AFF_1: 5;

                then (a1,a4) // (a2,a4) by A44, A45, AFF_1: 5;

                then (a4,a2) // (a4,a1) by AFF_1: 4;

                then LIN (a4,a2,a1) by AFF_1:def 1;

                hence contradiction by A5, A12, A13, A20, A29, AFF_1: 25;

              end;

              then

              consider c1 such that

               A48: LIN (b2,e1,c1) and

               A49: LIN (a2,e2,c1) by AFF_1: 60;

              (a2,e2) // (a2,c1) by A49, AFF_1:def 1;

              then (a2,a4) // (a2,c1) by A44, A45, AFF_1: 5;

              then

               A50: LIN (a2,a4,c1) by AFF_1:def 1;

              take c1;

              (b2,e1) // (b2,c1) by A48, AFF_1:def 1;

              hence thesis by A5, A12, A13, A29, A46, A47, A50, AFF_1: 5, AFF_1: 25;

            end;

            consider c2 such that

             A51: c2 in M and

             A52: (a2,a3) // (b1,c2) by A35;

            consider c1 such that

             A53: c1 in N and

             A54: (a1,a4) // (b2,c1) by A43;

            (b1,b4) // (b2,c1) by A8, A16, A26, A54, AFF_1: 5;

            then

             A55: (b4,b1) // (b2,c1) by AFF_1: 4;

            

             A56: o <> c1 & o <> c2

            proof

               A57:

              now

                assume o = c2;

                then

                 A58: (o,b1) // (a2,a3) by A52, AFF_1: 4;

                (o,b1) // (a2,a4) by A5, A7, A12, A13, A14, AFF_1: 39, AFF_1: 41;

                then (a2,a4) // (a2,a3) by A6, A18, A58, AFF_1: 5;

                then LIN (a2,a4,a3) by AFF_1:def 1;

                hence contradiction by A5, A12, A13, A21, A29, AFF_1: 25;

              end;

               A59:

              now

                assume o = c1;

                then

                 A60: (o,b2) // (a1,a4) by A54, AFF_1: 4;

                (o,b2) // (a1,a3) by A4, A6, A8, A9, A10, AFF_1: 39, AFF_1: 41;

                then (a1,a3) // (a1,a4) by A7, A22, A60, AFF_1: 5;

                then LIN (a1,a3,a4) by AFF_1:def 1;

                hence contradiction by A4, A8, A9, A16, A28, AFF_1: 25;

              end;

              assume not thesis;

              hence contradiction by A59, A57;

            end;

            (a3,a2) // (c2,b1) by A52, AFF_1: 4;

            then (b3,b2) // (c2,b1) by A9, A17, A24, AFF_1: 5;

            then (b2,b3) // (c2,b1) by AFF_1: 4;

            then

             A61: (b4,b3) // (c2,c1) by A2, A4, A5, A6, A7, A10, A11, A14, A15, A18, A19, A22, A23, A53, A51, A56, A55, AFF_2:def 2;

             LIN (a1,a2,d) by A31, AFF_1: 6;

            then (a1,a2) // (a1,d) by AFF_1:def 1;

            then (a2,a1) // (a1,d) by AFF_1: 4;

            then

             A62: (b2,b1) // (a1,d) by A8, A17, A25, AFF_1: 5;

            

             A63: b1 <> b3

            proof

              assume b1 = b3;

              then (b2,b1) // (a2,a3) by A24, AFF_1: 4;

              then

               A64: (a2,a1) // (a2,a3) by A10, A18, A25, AFF_1: 5;

              (o,a1) // (o,a3) by A4, A6, A8, A9, AFF_1: 39, AFF_1: 41;

              then LIN (o,a1,a3) by AFF_1:def 1;

              hence contradiction by A5, A6, A7, A12, A17, A20, A28, A64, AFF_1: 14, AFF_1: 25;

            end;

            

             A65: c1 <> c2

            proof

              

               A66: b1 <> c1

              proof

                assume b1 = c1;

                then (a1,a4) // (a2,a1) by A10, A18, A25, A54, AFF_1: 5;

                then (a1,a4) // (a1,a2) by AFF_1: 4;

                then LIN (a1,a4,a2) by AFF_1:def 1;

                then LIN (a2,a4,a1) by AFF_1: 6;

                hence contradiction by A5, A12, A13, A20, A29, AFF_1: 25;

              end;

              assume c1 = c2;

              then (a3,a2) // (b1,c1) by A52, AFF_1: 4;

              then

               A67: (b3,b2) // (b1,c1) by A9, A17, A24, AFF_1: 5;

              (b1,c1) // (b3,b1) by A5, A14, A15, A53, AFF_1: 39, AFF_1: 41;

              then (b3,b1) // (b3,b2) by A67, A66, AFF_1: 5;

              then LIN (b3,b1,b2) by AFF_1:def 1;

              hence contradiction by A5, A14, A15, A22, A63, AFF_1: 25;

            end;

             LIN (o,d,d) by AFF_1: 7;

            then

            consider Y such that

             A68: Y is being_line and

             A69: o in Y and

             A70: d in Y and d in Y by AFF_1: 21;

            

             A71: M <> N & M <> Y & N <> Y

            proof

               A72:

              now

                assume

                 A73: N = Y;

                 LIN (a2,d,a1) by A31, AFF_1: 6;

                hence contradiction by A5, A12, A20, A32, A70, A73, AFF_1: 25;

              end;

               A74:

              now

                assume

                 A75: M = Y;

                 LIN (a1,d,a2) by A31, AFF_1: 6;

                hence contradiction by A4, A8, A17, A33, A70, A75, AFF_1: 25;

              end;

              assume not thesis;

              hence contradiction by A13, A16, A74, A72;

            end;

            

             A76: o <> d

            proof

              assume o = d;

              then LIN (o,a1,a2) by A31, AFF_1: 6;

              hence contradiction by A4, A6, A7, A8, A17, A20, AFF_1: 25;

            end;

            ex d1 st LIN (b1,b2,d1) & d1 in Y

            proof

              consider e2 such that

               A77: (o,d) // (o,e2) and

               A78: o <> e2 by DIRAF: 40;

              consider e1 such that

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

               A80: b1 <> e1 by DIRAF: 40;

               not (b1,e1) // (o,e2)

              proof

                assume (b1,e1) // (o,e2);

                then (b1,b2) // (o,e2) by A79, A80, AFF_1: 5;

                then (b1,b2) // (o,d) by A77, A78, AFF_1: 5;

                then (b2,b1) // (o,d) by AFF_1: 4;

                then

                 A81: (a2,a1) // (o,d) by A10, A18, A25, AFF_1: 5;

                (a2,a1) // (a2,d) by A31, AFF_1:def 1;

                then (a2,d) // (o,d) by A8, A17, A81, AFF_1: 5;

                then (d,o) // (d,a2) by AFF_1: 4;

                then LIN (d,o,a2) by AFF_1:def 1;

                then

                 A82: LIN (o,a2,d) by AFF_1: 6;

                 LIN (a1,a2,d) by A31, AFF_1: 6;

                then (a1,a2) // (a1,d) by AFF_1:def 1;

                hence contradiction by A4, A6, A7, A8, A17, A20, A32, A82, AFF_1: 14, AFF_1: 25;

              end;

              then

              consider d1 such that

               A83: LIN (b1,e1,d1) and

               A84: LIN (o,e2,d1) by AFF_1: 60;

              (o,e2) // (o,d1) by A84, AFF_1:def 1;

              then (o,d) // (o,d1) by A77, A78, AFF_1: 5;

              then

               A85: LIN (o,d,d1) by AFF_1:def 1;

              take d1;

              (b1,e1) // (b1,d1) by A83, AFF_1:def 1;

              then (b1,b2) // (b1,d1) by A79, A80, AFF_1: 5;

              hence thesis by A76, A68, A69, A70, A85, AFF_1: 25, AFF_1:def 1;

            end;

            then

            consider d1 such that

             A86: LIN (b1,b2,d1) and

             A87: d1 in Y;

             LIN (b2,b1,d1) by A86, AFF_1: 6;

            then (b2,b1) // (b2,d1) by AFF_1:def 1;

            then (a1,d) // (b2,d1) by A10, A18, A62, AFF_1: 5;

            then

             A88: (d,a4) // (d1,c1) by A3, A4, A5, A6, A7, A8, A10, A13, A16, A20, A76, A68, A69, A70, A87, A53, A54, A71, AFF_2:def 4;

            (b1,b2) // (b1,d1) by A86, AFF_1:def 1;

            then (b2,b1) // (b1,d1) by AFF_1: 4;

            then (a2,a1) // (b1,d1) by A10, A18, A25, AFF_1: 5;

            then (a2,d) // (b1,d1) by A8, A17, A34, AFF_1: 5;

            then (d,a3) // (d1,c2) by A3, A4, A5, A6, A7, A9, A12, A14, A17, A21, A76, A68, A69, A70, A87, A51, A52, A71, AFF_2:def 4;

            then (a3,a4) // (c2,c1) by A3, A4, A5, A6, A7, A9, A13, A16, A21, A76, A68, A69, A70, A87, A53, A51, A71, A88, AFF_2:def 4;

            then (b4,b3) // (a3,a4) by A65, A61, AFF_1: 5;

            hence (a3,a4) // (b3,b4) by AFF_1: 4;

          end;

          now

             A89:

            now

              (o,b2) // (o,b4) by A4, A6, A10, A11, AFF_1: 39, AFF_1: 41;

              then

               A90: LIN (o,b2,b4) by AFF_1:def 1;

              assume

               A91: a2 = a4;

              then (a1,a4) // (b1,b2) by A25, AFF_1: 4;

              then (b1,b2) // (b1,b4) by A8, A16, A26, AFF_1: 5;

              hence (a3,a4) // (b3,b4) by A5, A6, A7, A14, A18, A22, A24, A91, A90, AFF_1: 14, AFF_1: 25;

            end;

             A92:

            now

              (o,b1) // (o,b3) by A5, A7, A14, A15, AFF_1: 39, AFF_1: 41;

              then

               A93: LIN (o,b1,b3) by AFF_1:def 1;

              assume

               A94: a1 = a3;

              then (a2,a1) // (b2,b3) by A24, AFF_1: 4;

              then (b2,b1) // (b2,b3) by A8, A17, A25, AFF_1: 5;

              hence (a3,a4) // (b3,b4) by A4, A6, A7, A10, A18, A22, A26, A94, A93, AFF_1: 14, AFF_1: 25;

            end;

            assume a1 = a3 or a2 = a4;

            hence (a3,a4) // (b3,b4) by A92, A89;

          end;

          hence (a3,a4) // (b3,b4) by A27;

        end;

        hence thesis;

      end;

      X is satisfying_major_indirect_Scherungssatz implies X is Pappian

      proof

        assume

         A95: X is satisfying_major_indirect_Scherungssatz;

        now

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

          assume that

           A96: M is being_line and

           A97: N is being_line and

           A98: M <> N and

           A99: o in M and

           A100: o in N and

           A101: o <> a and

           A102: o <> a1 and

           A103: o <> b and

           A104: o <> b1 and

           A105: o <> c and

           A106: o <> c1 and

           A107: a in M and

           A108: b in M and

           A109: c in M and

           A110: a1 in N and

           A111: b1 in N and

           A112: c1 in N and

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

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

          

           A115: not a in N & not b in N & not c in N & not a1 in M & not b1 in M & not c1 in M

          proof

            

             A116: (o,c1) // (o,c1) by AFF_1: 2;

            

             A117: (o,b1) // (o,b1) by AFF_1: 2;

            

             A118: (o,a1) // (o,a1) by AFF_1: 2;

            

             A119: (o,c) // (o,c) by AFF_1: 2;

            

             A120: (o,b) // (o,b) by AFF_1: 2;

            

             A121: (o,a) // (o,a) by AFF_1: 2;

            assume not thesis;

            then M // N by A96, A97, A99, A100, A101, A102, A103, A104, A105, A106, A107, A108, A109, A110, A111, A112, A121, A120, A119, A118, A117, A116, AFF_1: 38;

            hence contradiction by A98, A99, A100, AFF_1: 45;

          end;

          

           A122: (b,c1) // (b1,c) by A114, AFF_1: 4;

          

           A123: (b1,b) // (b,b1) by AFF_1: 2;

          (a,b1) // (a1,b) by A113, AFF_1: 4;

          then (a,c1) // (a1,c) by A95, A96, A97, A99, A100, A107, A108, A109, A110, A111, A112, A115, A122, A123;

          hence (a,c1) // (c,a1) by AFF_1: 4;

        end;

        hence thesis by AFF_2:def 2;

      end;

      hence thesis by A1;

    end;

    theorem :: CONMETR1:11

    X is satisfying_PPAP iff X is satisfying_indirect_Scherungssatz

    proof

      

       A1: X is satisfying_PPAP implies X is satisfying_indirect_Scherungssatz

      proof

        assume

         A2: X is satisfying_PPAP;

        then X is satisfying_pap by AFF_2: 10;

        then

         A3: X is satisfying_minor_indirect_Scherungssatz by Th9;

        X is Pappian by A2, AFF_2: 10;

        then X is satisfying_major_indirect_Scherungssatz by Th10;

        hence thesis by A3, Th1;

      end;

      X is satisfying_indirect_Scherungssatz implies X is satisfying_PPAP

      proof

        assume

         A4: X is satisfying_indirect_Scherungssatz;

        then X is satisfying_major_indirect_Scherungssatz;

        then

         A5: X is Pappian by Th10;

        X is satisfying_minor_indirect_Scherungssatz by A4, Th1;

        then X is satisfying_pap by Th9;

        hence thesis by A5, AFF_2: 10;

      end;

      hence thesis by A1;

    end;

    theorem :: CONMETR1:12

    X is satisfying_major_indirect_Scherungssatz implies X is satisfying_minor_indirect_Scherungssatz

    proof

      assume X is satisfying_major_indirect_Scherungssatz;

      then X is Pappian by Th10;

      then X is satisfying_pap by AFF_2: 9;

      hence thesis by Th9;

    end;

    reserve X for OrtAfPl;

    reserve o9,a9,a19,a29,a39,a49,b9,b19,b29,b39,b49,c9,c19 for Element of X;

    reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1 for Element of the AffinStruct of X;

    reserve M9,N9 for Subset of X;

    reserve A,M,N for Subset of the AffinStruct of X;

    theorem :: CONMETR1:13

     the AffinStruct of X is satisfying_Scherungssatz iff X is satisfying_SCH

    proof

      

       A1: X is satisfying_SCH implies the AffinStruct of X is satisfying_Scherungssatz

      proof

        assume

         A2: X is satisfying_SCH;

        now

          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 X;

          

           A24: (a39,a29) // (b39,b29) by A21, ANALMETR: 36;

          

           A25: (a19,a49) // (b19,b49) by A23, ANALMETR: 36;

          

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

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

          

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

          M9 is being_line by A3, ANALMETR: 43;

          then (a39,a49) // (b39,b49) by A2, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A27, A24, A26, A25, CONMETR:def 6;

          hence (a3,a4) // (b3,b4) by ANALMETR: 36;

        end;

        hence thesis;

      end;

       the AffinStruct of X is satisfying_Scherungssatz implies X is satisfying_SCH

      proof

        assume

         A28: the AffinStruct of X is satisfying_Scherungssatz;

        now

          let a19, a29, a39, a49, b19, b29, b39, b49, M9, N9;

          assume that

           A29: M9 is being_line and

           A30: N9 is being_line and

           A31: a19 in M9 and

           A32: a39 in M9 and

           A33: b19 in M9 and

           A34: b39 in M9 and

           A35: a29 in N9 and

           A36: a49 in N9 and

           A37: b29 in N9 and

           A38: b49 in N9 and

           A39: not a49 in M9 and

           A40: not a29 in M9 and

           A41: not b29 in M9 and

           A42: not b49 in M9 and

           A43: not a19 in N9 and

           A44: not a39 in N9 and

           A45: not b19 in N9 and

           A46: not b39 in N9 and

           A47: (a39,a29) // (b39,b29) and

           A48: (a29,a19) // (b29,b19) and

           A49: (a19,a49) // (b19,b49);

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

          

           A50: (a3,a2) // (b3,b2) by A47, ANALMETR: 36;

          

           A51: (a1,a4) // (b1,b4) by A49, ANALMETR: 36;

          

           A52: (a2,a1) // (b2,b1) by A48, ANALMETR: 36;

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

          

           A53: N is being_line by A30, ANALMETR: 43;

          M is being_line by A29, ANALMETR: 43;

          then (a3,a4) // (b3,b4) by A28, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A45, A46, A53, A50, A52, A51;

          hence (a39,a49) // (b39,b49) by ANALMETR: 36;

        end;

        hence thesis by CONMETR:def 6;

      end;

      hence thesis by A1;

    end;

    theorem :: CONMETR1:14

    X is satisfying_TDES iff the AffinStruct of X is Moufangian

    proof

       the AffinStruct of X is Moufangian implies X is satisfying_TDES

      proof

        assume

         A1: the AffinStruct of X is Moufangian;

        now

          let o9, a9, a19, b9, b19, c9, c19;

          assume that o9 <> a9 and o9 <> a19 and

           A2: o9 <> b9 and o9 <> b19 and

           A3: o9 <> c9 and o9 <> c19 and

           A4: not LIN (b9,b19,a9) and

           A5: not LIN (b9,b19,c9) and

           A6: LIN (o9,a9,a19) and

           A7: LIN (o9,b9,b19) and

           A8: LIN (o9,c9,c19) and

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

           A10: (a9,b9) // (o9,c9) and

           A11: (b9,c9) // (b19,c19);

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

          

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

           LIN (o,c,c1) by A8, ANALMETR: 40;

          then

          consider M such that

           A13: M is being_line and

           A14: o in M and

           A15: c in M and

           A16: c1 in M by AFF_1: 21;

          

           A17: not LIN (b,b1,c) by A5, ANALMETR: 40;

          

           A18: not b in M

          proof

             LIN (b,b1,o) by A12, AFF_1: 6;

            then (b,b1) // (b,o) by AFF_1:def 1;

            then

             A19: (b,b1) // (o,b) by AFF_1: 4;

            assume b in M;

            then (o,b) // (b,c) by A13, A14, A15, AFF_1: 39, AFF_1: 41;

            then (b,b1) // (b,c) by A2, A19, AFF_1: 5;

            hence contradiction by A17, AFF_1:def 1;

          end;

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

          then

           A20: (b,a) // (b1,a1) by AFF_1: 4;

           not LIN (b,b1,a) by A4, ANALMETR: 40;

          then

           A21: b <> a by AFF_1: 7;

          

           A22: (b,c) // (b1,c1) by A11, ANALMETR: 36;

          

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

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

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

          then (b,a) // M by A3, A13, A14, A15, AFF_1: 27;

          then (a,c) // (a1,c1) by A1, A3, A23, A12, A13, A14, A15, A16, A18, A21, A20, A22, AFF_2:def 7;

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

        end;

        hence thesis by CONMETR:def 5;

      end;

      hence thesis by CONMETR: 7;

    end;

    theorem :: CONMETR1:15

     the AffinStruct of X is translational iff X is satisfying_des

    proof

      X is satisfying_des implies the AffinStruct of X is translational

      proof

        assume

         A1: X is satisfying_des;

        now

          let A, M, N, a, b, c, a1, b1, c1;

          assume that

           A2: A // M and

           A3: A // N and

           A4: a in A and

           A5: a1 in A and

           A6: b in M and

           A7: b1 in M and

           A8: c in N and

           A9: c1 in N and

           A10: A is being_line and

           A11: M is being_line and

           A12: N is being_line and

           A13: A <> M and

           A14: A <> N and

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

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

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

          (b,c) // (b1,c1)

          proof

            assume

             A17: not (b,c) // (b1,c1);

            

             A18: a <> a1

            proof

              assume

               A19: a = a1;

              

               A20: c = c1

              proof

                 LIN (a,c,c1) by A16, A19, AFF_1:def 1;

                then

                 A21: LIN (c,c1,a) by AFF_1: 6;

                assume c <> c1;

                then a in N by A8, A9, A12, A21, AFF_1: 25;

                hence contradiction by A3, A4, A14, AFF_1: 45;

              end;

              b = b1

              proof

                 LIN (a,b,b1) by A15, A19, AFF_1:def 1;

                then

                 A22: LIN (b,b1,a) by AFF_1: 6;

                assume b <> b1;

                then a in M by A6, A7, A11, A22, AFF_1: 25;

                hence contradiction by A2, A4, A13, AFF_1: 45;

              end;

              hence contradiction by A17, A20, AFF_1: 2;

            end;

            

             A23: not LIN (a9,a19,b9) & not LIN (a9,a19,c9)

            proof

              assume LIN (a9,a19,b9) or LIN (a9,a19,c9);

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

              then b in A or c in A by A4, A5, A10, A18, AFF_1: 25;

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

            end;

            (a,a1) // (c,c1) by A3, A4, A5, A8, A9, AFF_1: 39;

            then

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

            (a,a1) // (b,b1) by A2, A4, A5, A6, A7, AFF_1: 39;

            then

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

            

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

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

            then (b9,c9) // (b19,c19) by A1, A23, A25, A24, A26, CONMETR:def 8;

            hence contradiction by A17, ANALMETR: 36;

          end;

          hence (b,c) // (b1,c1);

        end;

        hence thesis by AFF_2:def 11;

      end;

      hence thesis by CONMETR: 8;

    end;

    theorem :: CONMETR1:16

    X is satisfying_PAP iff the AffinStruct of X is Pappian

    proof

      

       A1: X is satisfying_PAP implies the AffinStruct of X is Pappian

      proof

        assume

         A2: X is satisfying_PAP;

        now

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

          assume that

           A3: M is being_line and

           A4: N is being_line and

           A5: M <> N and

           A6: o in M and

           A7: o in N and

           A8: o <> a and

           A9: o <> a1 and

           A10: o <> b and

           A11: o <> b1 and

           A12: o <> c and

           A13: o <> c1 and

           A14: a in M and

           A15: b in M and

           A16: c in M and

           A17: a1 in N and

           A18: b1 in N and

           A19: c1 in N and

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

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

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

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

          

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

          

           A23: not c19 in M9 & not b9 in N9

          proof

            assume c19 in M9 or b9 in N9;

            then

             A24: (o,c1) // M or (o,b) // N by A3, A4, A6, A7, AFF_1: 52;

            

             A25: (o,b) // M by A3, A6, A15, AFF_1: 52;

            (o,c1) // N by A4, A7, A19, AFF_1: 52;

            hence contradiction by A5, A6, A7, A10, A13, A24, A25, AFF_1: 45, AFF_1: 53;

          end;

          (b,a1) // (a,b1) by A20, AFF_1: 4;

          then

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

          

           A27: (b9,c19) // (c9,b19) by A21, ANALMETR: 36;

          M9 is being_line by A3, ANALMETR: 43;

          then (a9,c19) // (c9,a19) by A2, A6, A7, A8, A9, A11, A12, A14, A15, A16, A17, A18, A19, A22, A26, A27, A23, CONMETR:def 2;

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

        end;

        hence thesis by AFF_2:def 2;

      end;

       the AffinStruct of X is Pappian implies X is satisfying_PAP

      proof

        assume

         A28: the AffinStruct of X is Pappian;

        now

          let o9, a19, a29, a39, b19, b29, b39, M9, N9;

          assume that

           A29: M9 is being_line and

           A30: N9 is being_line and

           A31: o9 in M9 and

           A32: a19 in M9 and

           A33: a29 in M9 and

           A34: a39 in M9 and

           A35: o9 in N9 and

           A36: b19 in N9 and

           A37: b29 in N9 and

           A38: b39 in N9 and

           A39: not b29 in M9 and

           A40: not a39 in N9 and

           A41: o9 <> a19 and

           A42: o9 <> a29 and o9 <> a39 and

           A43: o9 <> b19 and o9 <> b29 and

           A44: o9 <> b39 and

           A45: (a39,b29) // (a29,b19) and

           A46: (a39,b39) // (a19,b19);

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

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

          

           A47: N is being_line by A30, ANALMETR: 43;

          

           A48: M is being_line by A29, ANALMETR: 43;

          now

            assume M <> N;

            (a3,b3) // (a1,b1) by A46, ANALMETR: 36;

            then

             A49: (a1,b1) // (a3,b3) by AFF_1: 4;

            (a3,b2) // (a2,b1) by A45, ANALMETR: 36;

            then (a1,b2) // (a2,b3) by A28, A31, A32, A33, A34, A35, A36, A37, A38, A39, A40, A41, A42, A43, A44, A48, A47, A49, AFF_2:def 2;

            hence (a19,b29) // (a29,b39) by ANALMETR: 36;

          end;

          hence (a19,b29) // (a29,b39) by A37, A39;

        end;

        hence thesis by CONMETR:def 2;

      end;

      hence thesis by A1;

    end;

    theorem :: CONMETR1:17

    X is satisfying_DES iff the AffinStruct of X is Desarguesian

    proof

      

       A1: X is satisfying_DES implies the AffinStruct of X is Desarguesian

      proof

        assume

         A2: X is satisfying_DES;

        now

          let A, M, N, o, a, b, c, a1, b1, c1;

          assume that

           A3: o in A and

           A4: o in M and

           A5: o in N and

           A6: o <> a and

           A7: o <> b and

           A8: o <> c and

           A9: a in A and

           A10: a1 in A and

           A11: b in M and

           A12: b1 in M and

           A13: c in N and

           A14: c1 in N and

           A15: A is being_line and

           A16: M is being_line and

           A17: N is being_line and

           A18: A <> M and

           A19: A <> N and

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

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

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

          (o,b) // (o,b1) by A4, A11, A12, A16, AFF_1: 39, AFF_1: 41;

          then

           A22: LIN (o,b,b1) by AFF_1:def 1;

          then

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

          (o,a) // (o,a1) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

          then

           A24: LIN (o,a,a1) by AFF_1:def 1;

          (o,c) // (o,c1) by A5, A13, A14, A17, AFF_1: 39, AFF_1: 41;

          then

           A25: LIN (o,c,c1) by AFF_1:def 1;

          then

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

          assume

           A27: not (b,c) // (b1,c1);

          

           A28: not LIN (b9,b19,a9) & not LIN (a9,a19,c9)

          proof

            

             A29: a <> a1

            proof

              assume

               A30: a = a1;

              

               A31: c = c1

              proof

                

                 A32: not LIN (o,a,c)

                proof

                  assume LIN (o,a,c);

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

                  then

                   A33: (o,c) // A by A3, A15, AFF_1: 52;

                  (o,c) // N by A5, A13, A17, AFF_1: 52;

                  hence contradiction by A3, A5, A8, A19, A33, AFF_1: 45, AFF_1: 53;

                end;

                assume c <> c1;

                hence contradiction by A21, A25, A30, A32, AFF_1: 14;

              end;

              b = b1

              proof

                

                 A34: not LIN (o,a,b)

                proof

                  assume LIN (o,a,b);

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

                  then

                   A35: (o,b) // A by A3, A15, AFF_1: 52;

                  (o,b) // M by A4, A11, A16, AFF_1: 52;

                  hence contradiction by A3, A4, A7, A18, A35, AFF_1: 45, AFF_1: 53;

                end;

                assume b <> b1;

                hence contradiction by A20, A22, A30, A34, AFF_1: 14;

              end;

              hence contradiction by A27, A31, AFF_1: 2;

            end;

            

             A36: b <> b1

            proof

              

               A37: not LIN (o,b,a)

              proof

                assume LIN (o,b,a);

                then a in M by A4, A7, A11, A16, AFF_1: 25;

                then

                 A38: (o,a) // M by A4, A16, AFF_1: 52;

                (o,a) // A by A3, A9, A15, AFF_1: 52;

                hence contradiction by A3, A4, A6, A18, A38, AFF_1: 45, AFF_1: 53;

              end;

              assume b = b1;

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

              hence contradiction by A24, A29, A37, AFF_1: 14;

            end;

            assume LIN (b9,b19,a9) or LIN (a9,a19,c9);

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

            then a in M or c in A by A9, A10, A11, A12, A15, A16, A29, A36, AFF_1: 25;

            then

             A39: (o,a) // M or (o,c) // A by A3, A4, A15, A16, AFF_1: 52;

            

             A40: (o,c) // N by A5, A13, A17, AFF_1: 52;

            (o,a) // A by A3, A9, A15, AFF_1: 52;

            hence contradiction by A3, A4, A5, A6, A8, A18, A19, A39, A40, AFF_1: 45, AFF_1: 53;

          end;

          

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

          

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

          

           A43: o9 <> a19 & o9 <> b19 & o9 <> c19

          proof

             A44:

            now

              assume

               A45: o9 = a19;

              

               A46: o = c1

              proof

                

                 A47: not LIN (c,a,o)

                proof

                  assume LIN (c,a,o);

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

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

                  then

                   A48: (o,c) // A by A3, A15, AFF_1: 52;

                  (o,c) // N by A5, A13, A17, AFF_1: 52;

                  hence contradiction by A3, A5, A8, A19, A48, AFF_1: 45, AFF_1: 53;

                end;

                assume

                 A49: o <> c1;

                

                 A50: (o,c) // (o,c1) by A5, A13, A14, A17, AFF_1: 39, AFF_1: 41;

                then (a,c) // (o,c) by A21, A45, A49, AFF_1: 5;

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

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

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

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

                then (o,a) // (o,c1) by A8, A50, AFF_1: 5;

                then LIN (o,a,c1) by AFF_1:def 1;

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

                then

                 A51: (a,o) // (a,c1) by AFF_1:def 1;

                 LIN (c,o,c1) by A25, AFF_1: 6;

                hence contradiction by A49, A47, A51, AFF_1: 14;

              end;

              o = b1

              proof

                

                 A52: not LIN (b,a,o)

                proof

                  assume LIN (b,a,o);

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

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

                  then

                   A53: (o,b) // A by A3, A15, AFF_1: 52;

                  (o,b) // M by A4, A11, A16, AFF_1: 52;

                  hence contradiction by A3, A4, A7, A18, A53, AFF_1: 45, AFF_1: 53;

                end;

                assume

                 A54: o <> b1;

                

                 A55: (o,b1) // (o,b) by A4, A11, A12, A16, AFF_1: 39, AFF_1: 41;

                then (a,b) // (o,b) by A20, A45, A54, AFF_1: 5;

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

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

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

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

                then (o,a) // (o,b1) by A7, A55, AFF_1: 5;

                then LIN (o,a,b1) by AFF_1:def 1;

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

                then

                 A56: (a,o) // (a,b1) by AFF_1:def 1;

                 LIN (b,o,b1) by A22, AFF_1: 6;

                hence contradiction by A54, A52, A56, AFF_1: 14;

              end;

              hence contradiction by A27, A46, AFF_1: 3;

            end;

             A57:

            now

              

               A58: not LIN (a,b,o)

              proof

                assume LIN (a,b,o);

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

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

                then

                 A59: (o,b) // A by A3, A15, AFF_1: 52;

                (o,b) // M by A4, A11, A16, AFF_1: 52;

                hence contradiction by A3, A4, A7, A18, A59, AFF_1: 45, AFF_1: 53;

              end;

              

               A60: (a1,o) // (a,o) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

              assume o9 = b19;

              then (a,b) // (a,o) by A20, A44, A60, AFF_1: 5;

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

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

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

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

              then (o,b) // (a1,o) by A6, A60, AFF_1: 5;

              then (o,b) // (o,a1) by AFF_1: 4;

              then LIN (o,b,a1) by AFF_1:def 1;

              then LIN (b,o,a1) by AFF_1: 6;

              then

               A61: (b,o) // (b,a1) by AFF_1:def 1;

               LIN (a,o,a1) by A24, AFF_1: 6;

              hence contradiction by A44, A58, A61, AFF_1: 14;

            end;

             A62:

            now

              

               A63: not LIN (a,c,o)

              proof

                assume LIN (a,c,o);

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

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

                then

                 A64: (o,c) // A by A3, A15, AFF_1: 52;

                (o,c) // N by A5, A13, A17, AFF_1: 52;

                hence contradiction by A3, A5, A8, A19, A64, AFF_1: 45, AFF_1: 53;

              end;

              

               A65: (a1,o) // (a,o) by A3, A9, A10, A15, AFF_1: 39, AFF_1: 41;

              assume o9 = c19;

              then (a,c) // (a,o) by A21, A44, A65, AFF_1: 5;

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

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

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

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

              then (o,c) // (a1,o) by A6, A65, AFF_1: 5;

              then (o,c) // (o,a1) by AFF_1: 4;

              then LIN (o,c,a1) by AFF_1:def 1;

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

              then

               A66: (c,o) // (c,a1) by AFF_1:def 1;

               LIN (a,o,a1) by A24, AFF_1: 6;

              hence contradiction by A44, A63, A66, AFF_1: 14;

            end;

            assume not thesis;

            hence contradiction by A44, A57, A62;

          end;

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

          then (b9,c9) // (b19,c19) by A2, A6, A7, A8, A23, A26, A43, A28, A42, A41, CONAFFM:def 1;

          hence contradiction by A27, ANALMETR: 36;

        end;

        hence thesis by AFF_2:def 4;

      end;

       the AffinStruct of X is Desarguesian implies X is satisfying_DES

      proof

        assume

         A67: the AffinStruct of X is Desarguesian;

        now

          let o9, a9, a19, b9, b19, c9, c19;

          assume that

           A68: o9 <> a9 and o9 <> a19 and

           A69: o9 <> b9 and o9 <> b19 and

           A70: o9 <> c9 and o9 <> c19 and

           A71: not LIN (b9,b19,a9) and

           A72: not LIN (a9,a19,c9) and

           A73: LIN (o9,a9,a19) and

           A74: LIN (o9,b9,b19) and

           A75: LIN (o9,c9,c19) and

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

           A77: (a9,c9) // (a19,c19);

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

          

           A78: not LIN (a,a1,c) by A72, ANALMETR: 40;

          

           A79: (a,c) // (a1,c1) by A77, ANALMETR: 36;

          

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

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

          then

          consider M such that

           A81: M is being_line and

           A82: o in M and

           A83: b in M and

           A84: b1 in M by AFF_1: 21;

           LIN (o,c,c1) by A75, ANALMETR: 40;

          then

          consider N such that

           A85: N is being_line and

           A86: o in N and

           A87: c in N and

           A88: c1 in N by AFF_1: 21;

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

          then

          consider A such that

           A89: A is being_line and

           A90: o in A and

           A91: a in A and

           A92: a1 in A by AFF_1: 21;

          

           A93: not LIN (b,b1,a) by A71, ANALMETR: 40;

          A <> M & A <> N

          proof

            assume not thesis;

            then (b,b1) // (b,a) or (a,a1) // (a,c) by A89, A91, A92, A83, A84, A87, AFF_1: 39, AFF_1: 41;

            hence contradiction by A93, A78, AFF_1:def 1;

          end;

          then (b,c) // (b1,c1) by A67, A68, A69, A70, A89, A90, A91, A92, A81, A82, A83, A84, A85, A86, A87, A88, A80, A79, AFF_2:def 4;

          hence (b9,c9) // (b19,c19) by ANALMETR: 36;

        end;

        hence thesis by CONAFFM:def 1;

      end;

      hence thesis by A1;

    end;