homothet.miz



    begin

    reserve AFP for AffinPlane;

    reserve a,a9,b,b9,c,c9,d,d9,o,p,p9,q,q9,r,s,t,x,y,z for Element of AFP;

    reserve A,A9,C,D,P,B9,M,N,K for Subset of AFP;

    reserve f for Permutation of the carrier of AFP;

    

     Lm1: AFP is Desarguesian iff for o, a, a9, p, p9, q, q9 st LIN (o,a,a9) & LIN (o,p,p9) & LIN (o,q,q9) & not LIN (o,a,p) & not LIN (o,a,q) & (a,p) // (a9,p9) & (a,q) // (a9,q9) holds (p,q) // (p9,q9)

    proof

      thus AFP is Desarguesian implies for o, a, a9, p, p9, q, q9 st LIN (o,a,a9) & LIN (o,p,p9) & LIN (o,q,q9) & not LIN (o,a,p) & not LIN (o,a,q) & (a,p) // (a9,p9) & (a,q) // (a9,q9) holds (p,q) // (p9,q9)

      proof

        assume

         A1: AFP is Desarguesian;

        let o, a, a9, p, p9, q, q9;

        assume that

         A2: LIN (o,a,a9) and

         A3: LIN (o,p,p9) and

         A4: LIN (o,q,q9) and

         A5: not LIN (o,a,p) and

         A6: not LIN (o,a,q) and

         A7: (a,p) // (a9,p9) and

         A8: (a,q) // (a9,q9);

        set A = ( Line (o,a)), P = ( Line (o,p)), C = ( Line (o,q));

        

         A9: a in A by AFF_1: 15;

        

         A10: o <> a by A5, AFF_1: 7;

        then

         A11: A is being_line by AFF_1:def 3;

        

         A12: o in A by AFF_1: 15;

        then

         A13: a9 in A by A2, A10, A11, A9, AFF_1: 25;

        

         A14: q in C by AFF_1: 15;

        then

         A15: A <> C by A6, A11, A12, A9, AFF_1: 21;

        

         A16: o in P by AFF_1: 15;

        

         A17: p in P by AFF_1: 15;

        

         A18: o <> p by A5, AFF_1: 7;

        then

         A19: P is being_line by AFF_1:def 3;

        then

         A20: p9 in P by A3, A18, A16, A17, AFF_1: 25;

        

         A21: o in C by AFF_1: 15;

        

         A22: o <> q by A6, AFF_1: 7;

        then

         A23: C is being_line by AFF_1:def 3;

        then

         A24: q9 in C by A4, A22, A21, A14, AFF_1: 25;

        A <> P by A5, A11, A12, A9, A17, AFF_1: 21;

        hence thesis by A1, A7, A8, A10, A18, A22, A11, A19, A23, A12, A9, A16, A17, A21, A14, A13, A20, A24, A15, AFF_2:def 4;

      end;

      assume

       A25: for o, a, a9, p, p9, q, q9 st LIN (o,a,a9) & LIN (o,p,p9) & LIN (o,q,q9) & not LIN (o,a,p) & not LIN (o,a,q) & (a,p) // (a9,p9) & (a,q) // (a9,q9) holds (p,q) // (p9,q9);

      now

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

        assume that

         A26: o in A and

         A27: o in P and

         A28: o in C and

         A29: o <> a and

         A30: o <> b and

         A31: o <> c and

         A32: a in A and

         A33: a9 in A and

         A34: b in P and

         A35: b9 in P and

         A36: c in C and

         A37: c9 in C and

         A38: A is being_line and

         A39: P is being_line and

         A40: C is being_line and

         A41: A <> P and

         A42: A <> C and

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

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

        

         A45: LIN (o,b,b9) by A27, A34, A35, A39, AFF_1: 21;

        

         A46: not LIN (o,a,c)

        proof

          assume LIN (o,a,c);

          then c in A by A26, A29, A32, A38, AFF_1: 25;

          hence contradiction by A26, A28, A31, A36, A38, A40, A42, AFF_1: 18;

        end;

        

         A47: not LIN (o,a,b)

        proof

          assume LIN (o,a,b);

          then b in A by A26, A29, A32, A38, AFF_1: 25;

          hence contradiction by A26, A27, A30, A34, A38, A39, A41, AFF_1: 18;

        end;

        

         A48: LIN (o,c,c9) by A28, A36, A37, A40, AFF_1: 21;

         LIN (o,a,a9) by A26, A32, A33, A38, AFF_1: 21;

        hence (b,c) // (b9,c9) by A25, A43, A44, A45, A48, A47, A46;

      end;

      hence thesis by AFF_2:def 4;

    end;

    

     Lm2: AFP is Moufangian iff for o, K, c, c9, a, b, a9, b9 st o in K & c in K & c9 in K & K is being_line & LIN (o,a,a9) & LIN (o,b,b9) & not a in K & (a,b) // K & (a9,b9) // K & (a,c) // (a9,c9) holds (b,c) // (b9,c9)

    proof

      thus AFP is Moufangian implies for o, K, c, c9, a, b, a9, b9 st o in K & c in K & c9 in K & K is being_line & LIN (o,a,a9) & LIN (o,b,b9) & not a in K & (a,b) // K & (a9,b9) // K & (a,c) // (a9,c9) holds (b,c) // (b9,c9)

      proof

        assume

         A1: AFP is Moufangian;

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

        assume that

         A2: o in K and

         A3: c in K and

         A4: c9 in K and

         A5: K is being_line and

         A6: LIN (o,a,a9) and

         A7: LIN (o,b,b9) and

         A8: not a in K and

         A9: (a,b) // K and

         A10: (a9,b9) // K and

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

        

         A12: (a,b) // (a9,b9) by A5, A9, A10, AFF_1: 31;

         A13:

        now

           A14:

          now

            assume

             A15: a = b;

             A16:

            now

              

               A17: not (o,a) // K by A2, A8, AFF_1: 34, AFF_1: 35;

              

               A18: LIN (o,b9,b) by A7, AFF_1: 6;

              assume that

               A19: (a9,o) // K and

               A20: a9 <> b9;

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

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

              then

               A21: (o,a) // K or a9 = o by A19, AFF_1: 32;

              then b9 in K by A2, A5, A8, A10, AFF_1: 23;

              hence contradiction by A2, A5, A8, A15, A20, A21, A17, A18, AFF_1: 25;

            end;

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

            then LIN (a9,b9,o) by A2, A6, A7, A8, A15, AFF_1: 8;

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

            hence thesis by A10, A11, A15, A16, AFF_1: 32;

          end;

          assume o <> c;

          hence thesis by A1, A2, A3, A4, A5, A6, A7, A8, A9, A11, A12, A14, AFF_2:def 7;

        end;

        now

          assume

           A22: o = c;

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

          then

           A23: (b,b9) // (b,c) by AFF_1:def 1;

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

          then LIN (a,c,c9) by A3, A8, A11, AFF_1: 9;

          then

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

          then LIN (c9,b,b9) by A2, A4, A5, A7, A8, A22, AFF_1: 25;

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

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

          then

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

          c = c9 by A3, A4, A5, A8, A24, AFF_1: 25;

          then b = b9 implies thesis by AFF_1: 2;

          hence thesis by A23, A25, AFF_1: 5;

        end;

        hence thesis by A13;

      end;

      assume

       A26: for o, K, c, c9, a, b, a9, b9 st o in K & c in K & c9 in K & K is being_line & LIN (o,a,a9) & LIN (o,b,b9) & not a in K & (a,b) // K & (a9,b9) // K & (a,c) // (a9,c9) holds (b,c) // (b9,c9);

      now

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

        assume that

         A27: K is being_line and

         A28: o in K and

         A29: c in K and

         A30: c9 in K and

         A31: not a in K and o <> c and

         A32: a <> b and

         A33: LIN (o,a,a9) and

         A34: LIN (o,b,b9) and

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

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

         A37: (a,b) // K;

        (a9,b9) // K by A32, A35, A37, AFF_1: 32;

        hence (b,c) // (b9,c9) by A26, A27, A28, A29, A30, A31, A33, A34, A36, A37;

      end;

      hence thesis by AFF_2:def 7;

    end;

    

     Lm3: AFP is Moufangian implies for K, o, a, b, c, a9, b9, c9 st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN (o,a,a9) & (a,b) // (a9,b9) & (b,c) // (b9,c9) & (a,c) // (a9,c9) & (a,b) // K holds LIN (o,b,b9)

    proof

      assume

       A1: AFP is Moufangian;

      thus for K, o, a, b, c, a9, b9, c9 st K is being_line & o in K & c in K & c9 in K & not a in K & a <> b & LIN (o,a,a9) & (a,b) // (a9,b9) & (b,c) // (b9,c9) & (a,c) // (a9,c9) & (a,b) // K holds LIN (o,b,b9)

      proof

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

        assume that

         A2: K is being_line and

         A3: o in K and

         A4: c in K and

         A5: c9 in K and

         A6: not a in K and

         A7: a <> b and

         A8: LIN (o,a,a9) and

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

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

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

         A12: (a,b) // K;

        consider P such that

         A13: a9 in P and

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

        

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

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

        

         A16: o in A by AFF_1: 15;

        

         A17: b in A by AFF_1: 15;

        assume

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

        then o <> b by AFF_1: 7;

        then

         A19: A is being_line by AFF_1:def 3;

        

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

         not A // P

        proof

          assume A // P;

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

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

        end;

        then

        consider x such that

         A21: x in A and

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

        

         A23: o in C by AFF_1: 15;

        (a,b) // P by A12, A14, AFF_1: 43;

        then (a9,b9) // P by A7, A9, AFF_1: 32;

        then

         A24: b9 in P by A13, A15, AFF_1: 23;

        then

         A25: LIN (b9,x,b9) by A15, A22, AFF_1: 21;

        

         A26: a in C by AFF_1: 15;

        

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

        

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

        then

         A29: a9 in C by A3, A6, A8, A23, A26, AFF_1: 25;

        

         A30: b9 <> c9

        proof

          

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

          assume

           A32: b9 = c9;

          then P = K by A5, A14, A24, AFF_1: 45;

          then a9 = o by A2, A3, A6, A28, A23, A26, A29, A13, AFF_1: 18;

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

          hence contradiction by A18, AFF_1: 7;

        end;

        

         A33: a9 <> b9

        proof

          assume

           A34: a9 = b9;

           A35:

          now

            assume a9 = c9;

            then b9 = o by A2, A3, A5, A6, A28, A23, A26, A29, A34, AFF_1: 18;

            hence contradiction by A18, AFF_1: 7;

          end;

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

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

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

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

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

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

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

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

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

        end;

        

         A36: b <> c by A4, A6, A12, AFF_1: 35;

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

        then (b,c) // (x,c9) by A1, A2, A3, A4, A5, A6, A8, A11, A12, A27, Lm2;

        then (b9,c9) // (x,c9) by A10, A36, AFF_1: 5;

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

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

        then

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

         LIN (b9,x,a9) by A13, A15, A22, A24, AFF_1: 21;

        then LIN (b9,c9,a9) by A18, A27, A37, A25, AFF_1: 8;

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

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

        then (b,c) // (a9,b9) by A10, A30, AFF_1: 5;

        then (a,b) // (b,c) by A9, A33, AFF_1: 5;

        then (b,c) // K by A7, A12, AFF_1: 32;

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

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

      end;

    end;

    

     Lm4: AFP is Moufangian implies for K, A, C, p, q, a, a9, b, b9 st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a9 in A & b in C & b9 in C & (p,a) // (q,a9) & (p,b) // (q,b9) holds (a,b) // (a9,b9)

    proof

      assume AFP is Moufangian;

      then

       A1: AFP is translational by AFF_2: 14;

      let K, A, C, p, q, a, a9, b, b9;

      assume that

       A2: K // A and

       A3: K // C and

       A4: K <> A and

       A5: K <> C and

       A6: p in K and

       A7: q in K and

       A8: a in A and

       A9: a9 in A and

       A10: b in C and

       A11: b9 in C and

       A12: (p,a) // (q,a9) and

       A13: (p,b) // (q,b9);

      

       A14: A is being_line by A2, AFF_1: 36;

      

       A15: C is being_line by A3, AFF_1: 36;

      K is being_line by A2, AFF_1: 36;

      hence thesis by A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A1, A14, A15, AFF_2:def 11;

    end;

    theorem :: HOMOTHET:1

    

     Th1: not LIN (o,a,p) & LIN (o,a,b) & LIN (o,a,x) & LIN (o,a,y) & LIN (o,p,p9) & LIN (o,p,q) & LIN (o,p,q9) & p <> q & o <> q & o <> x & (a,p) // (b,p9) & (a,q) // (b,q9) & (x,p) // (y,p9) & AFP is Desarguesian implies (x,q) // (y,q9)

    proof

      assume that

       A1: not LIN (o,a,p) and

       A2: LIN (o,a,b) and

       A3: LIN (o,a,x) and

       A4: LIN (o,a,y) and

       A5: LIN (o,p,p9) and

       A6: LIN (o,p,q) and

       A7: LIN (o,p,q9) and

       A8: p <> q and

       A9: o <> q and

       A10: o <> x and

       A11: (a,p) // (b,p9) and

       A12: (a,q) // (b,q9) and

       A13: (x,p) // (y,p9) and

       A14: AFP is Desarguesian;

      set B9 = ( Line (o,p));

      

       A15: o in B9 by AFF_1: 15;

      

       A16: o <> p by A1, AFF_1: 7;

      then

      consider d such that

       A17: LIN (x,p,d) and

       A18: d <> x and

       A19: d <> p by A6, A8, A9, TRANSLAC: 1;

      

       A20: B9 is being_line by A16, AFF_1:def 3;

      

       A21: q9 in B9 by A7, AFF_1:def 2;

      q in B9 by A6, AFF_1:def 2;

      then

       A22: LIN (o,q,q9) by A20, A15, A21, AFF_1: 21;

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

      o <> a by A1, AFF_1: 7;

      then

       A23: A is being_line by AFF_1:def 3;

      

       A24: y in A by A4, AFF_1:def 2;

      

       A25: (p,a) // (p9,b) by A11, AFF_1: 4;

      

       A26: not LIN (o,p,a) by A1, AFF_1: 6;

      set K = ( Line (x,p));

      

       A27: K is being_line by A1, A3, AFF_1:def 3;

      then

      consider M such that

       A28: y in M and

       A29: K // M by AFF_1: 49;

      

       A30: x in K by AFF_1: 15;

      

       A31: M is being_line by A29, AFF_1: 36;

      

       A32: p in K by AFF_1: 15;

      

       A33: d in K by A17, AFF_1:def 2;

      

       A34: x in A by A3, AFF_1:def 2;

      

       A35: not LIN (o,a,d)

      proof

        assume LIN (o,a,d);

        then d in A by AFF_1:def 2;

        then A = K by A18, A27, A30, A33, A23, A34, AFF_1: 18;

        hence contradiction by A1, A32, AFF_1:def 2;

      end;

      

       A36: o in A by AFF_1: 15;

       not (o,d) // M

      proof

        assume (o,d) // M;

        then (o,d) // K by A29, AFF_1: 43;

        then (d,o) // K by AFF_1: 34;

        then o in K by A27, A33, AFF_1: 23;

        then A = K by A10, A27, A30, A23, A36, A34, AFF_1: 18;

        hence contradiction by A1, A32, AFF_1:def 2;

      end;

      then

      consider d9 such that

       A37: d9 in M and

       A38: LIN (o,d,d9) by A31, AFF_1: 59;

      

       A39: (d,x) // (d9,y) by A30, A33, A28, A29, A37, AFF_1: 39;

      

       A40: p in B9 by AFF_1: 15;

      

       A41: not LIN (o,d,q)

      proof

        assume LIN (o,d,q);

        then

         A42: LIN (o,q,d) by AFF_1: 6;

        

         A43: LIN (o,q,o) by AFF_1: 7;

         LIN (o,q,p) by A6, AFF_1: 6;

        then LIN (o,p,d) by A9, A43, A42, AFF_1: 8;

        then d in B9 by AFF_1:def 2;

        then B9 = K by A19, A27, A32, A33, A20, A40, AFF_1: 18;

        then A = B9 by A10, A27, A30, A23, A36, A34, A15, AFF_1: 18;

        hence contradiction by A1, A40, AFF_1:def 2;

      end;

      

       A44: not LIN (o,d,x)

      proof

        assume LIN (o,d,x);

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

        then d in A by A10, A23, A36, A34, AFF_1: 25;

        then A = K by A18, A27, A30, A33, A23, A34, AFF_1: 18;

        hence contradiction by A1, A32, AFF_1:def 2;

      end;

      

       A45: not LIN (o,p,d)

      proof

        assume LIN (o,p,d);

        then d in B9 by AFF_1:def 2;

        then K = B9 by A19, A27, A32, A33, A20, A40, AFF_1: 18;

        hence contradiction by A27, A30, A33, A15, A44, AFF_1: 21;

      end;

      

       A46: q in B9 by A6, AFF_1:def 2;

      

       A47: not LIN (o,a,q)

      proof

        assume LIN (o,a,q);

        then q in A by AFF_1:def 2;

        then A = B9 by A9, A23, A36, A20, A15, A46, AFF_1: 18;

        hence contradiction by A1, A40, AFF_1:def 2;

      end;

      x in A by A3, AFF_1:def 2;

      then

       A48: LIN (o,x,y) by A23, A36, A24, AFF_1: 21;

      (x,p) // K by A27, A30, A32, AFF_1: 23;

      then (x,p) // M by A29, AFF_1: 43;

      then (y,p9) // M by A1, A3, A13, AFF_1: 32;

      then p9 in M by A28, A31, AFF_1: 23;

      then (p,d) // (p9,d9) by A32, A33, A29, A37, AFF_1: 39;

      then (a,d) // (b,d9) by A2, A5, A14, A38, A45, A26, A25, Lm1;

      then (d,q) // (d9,q9) by A2, A12, A14, A38, A47, A35, A22, Lm1;

      hence thesis by A14, A38, A39, A41, A44, A22, A48, Lm1;

    end;

    theorem :: HOMOTHET:2

    

     Th2: (for o, a, b st o <> a & o <> b & LIN (o,a,b) holds ex f st f is dilatation & (f . o) = o & (f . a) = b) implies AFP is Desarguesian

    proof

      assume

       A1: for o, a, b st o <> a & o <> b & LIN (o,a,b) holds ex f st f is dilatation & (f . o) = o & (f . a) = b;

      now

        let o, a, a9, p, p9, q, q9;

        assume that

         A2: LIN (o,a,a9) and

         A3: LIN (o,p,p9) and

         A4: LIN (o,q,q9) and

         A5: not LIN (o,a,p) and

         A6: not LIN (o,a,q) and

         A7: (a,p) // (a9,p9) and

         A8: (a,q) // (a9,q9);

         A9:

        now

          assume

           A10: o <> a9;

          o <> a by A5, AFF_1: 7;

          then

          consider f such that

           A11: f is dilatation and

           A12: (f . o) = o and

           A13: (f . a) = a9 by A1, A2, A10;

          set s = (f . q);

          (o,q) // (o,s) by A11, A12, TRANSGEO: 68;

          then

           A14: LIN (o,q,s) by AFF_1:def 1;

          set r = (f . p);

          (o,p) // (o,r) by A11, A12, TRANSGEO: 68;

          then

           A15: LIN (o,p,r) by AFF_1:def 1;

          (a,q) // (a9,s) by A11, A13, TRANSGEO: 68;

          then

           A16: s = q9 by A2, A4, A6, A8, A14, AFF_1: 56;

          (a,p) // (a9,r) by A11, A13, TRANSGEO: 68;

          then r = p9 by A2, A3, A5, A7, A15, AFF_1: 56;

          hence (p,q) // (p9,q9) by A11, A16, TRANSGEO: 68;

        end;

        now

          assume

           A17: o = a9;

          then o = p9 by A3, A5, A7, AFF_1: 55;

          then p9 = q9 by A4, A6, A8, A17, AFF_1: 55;

          hence (p,q) // (p9,q9) by AFF_1: 3;

        end;

        hence (p,q) // (p9,q9) by A9;

      end;

      hence thesis by Lm1;

    end;

    

     Lm5: o <> a & o <> b & LIN (o,a,b) & LIN (o,a,y) & ( not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y))) implies LIN (o,a,x)

    proof

      assume that

       A1: o <> a and

       A2: o <> b and

       A3: LIN (o,a,b) and

       A4: LIN (o,a,y) and

       A5: not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y));

      assume

       A6: not LIN (o,a,x);

      then

       A7: b <> y by A2, A3, A5, AFF_1: 54;

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

      

       A8: A is being_line by A1, AFF_1:def 3;

      

       A9: (b,y) // (a,x) by A5, A6, AFF_1: 4;

      

       A10: a in A by AFF_1: 15;

      

       A11: y in A by A4, AFF_1:def 2;

      

       A12: o in A by AFF_1: 15;

      b in A by A3, AFF_1:def 2;

      then A = ( Line (b,y)) by A8, A7, A11, AFF_1: 24;

      then x in A by A7, A10, A9, AFF_1: 22;

      hence contradiction by A6, A8, A12, A10, AFF_1: 21;

    end;

    

     Lm6: o <> a & o <> b & LIN (o,a,b) & ( not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y))) implies o <> b & o <> a & LIN (o,b,a) & ( not LIN (o,b,y) & LIN (o,y,x) & (b,y) // (a,x) or ( LIN (o,b,y) & ex p, p9 st not LIN (o,b,p) & LIN (o,p,p9) & (b,p) // (a,p9) & (p,y) // (p9,x) & LIN (o,b,x)))

    proof

      assume that

       A1: o <> a and

       A2: o <> b and

       A3: LIN (o,a,b) and

       A4: not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y));

      

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

       A6:

      now

        assume

         A7: LIN (o,a,x);

        then

        consider p, q such that

         A8: not LIN (o,a,p) and

         A9: LIN (o,p,q) and

         A10: (a,p) // (b,q) and

         A11: (p,x) // (q,y) and

         A12: LIN (o,a,y) by A4;

        

         A13: not LIN (o,p,a) by A8, AFF_1: 6;

        

         A14: (q,y) // (p,x) by A11, AFF_1: 4;

        

         A15: (b,q) // (a,p) by A10, AFF_1: 4;

        

         A16: LIN (o,q,p) by A9, AFF_1: 6;

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

        then

         A17: LIN (o,b,x) by A1, A3, A7, AFF_1: 8;

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

        

         A18: o in A by AFF_1: 15;

        

         A19: a in A by A5, AFF_1:def 2;

        

         A20: A is being_line by A2, AFF_1:def 3;

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

        then

         A21: q <> o by A2, A3, A13, AFF_1: 55;

        

         A22: not LIN (o,b,q)

        proof

          assume LIN (o,b,q);

          then q in A by AFF_1:def 2;

          then p in A by A21, A20, A18, A16, AFF_1: 25;

          hence contradiction by A8, A20, A18, A19, AFF_1: 21;

        end;

        y in A by A1, A12, A20, A18, A19, AFF_1: 25;

        hence thesis by A1, A2, A3, A15, A14, A16, A22, A17, AFF_1: 6, AFF_1:def 2;

      end;

      now

        assume

         A23: not LIN (o,a,x);

        then

         A24: not LIN (o,a,y) by A1, A2, A3, A4, Lm5;

         not LIN (o,b,y)

        proof

          

           A25: LIN (o,b,o) by AFF_1: 7;

          assume

           A26: LIN (o,b,y);

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

          hence contradiction by A2, A24, A26, A25, AFF_1: 8;

        end;

        hence thesis by A1, A2, A3, A4, A23, AFF_1: 4, AFF_1: 6;

      end;

      hence thesis by A6;

    end;

    

     Lm7: o <> a & x = o & ( not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y))) implies y = o

    proof

      assume that

       A1: o <> a and

       A2: x = o and

       A3: not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y));

      consider p, p9 such that

       A4: not LIN (o,a,p) and

       A5: LIN (o,p,p9) and (a,p) // (b,p9) and

       A6: (p,x) // (p9,y) and

       A7: LIN (o,a,y) by A2, A3, AFF_1: 7;

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

      

       A8: o <> p by A4, AFF_1: 7;

      p9 in K by A5, AFF_1:def 2;

      then

       A9: y in K by A2, A6, A8, AFF_1: 22;

      assume

       A10: y <> o;

      

       A11: o in K by AFF_1: 15;

      

       A12: p in K by AFF_1: 15;

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

      

       A13: A is being_line by A1, AFF_1:def 3;

      

       A14: a in A by AFF_1: 15;

      

       A15: y in A by A7, AFF_1:def 2;

      

       A16: o in A by AFF_1: 15;

      K is being_line by A8, AFF_1:def 3;

      then p in A by A10, A13, A16, A12, A9, A11, A15, AFF_1: 18;

      hence contradiction by A4, A13, A16, A14, AFF_1: 21;

    end;

    

     Lm8: for o, a, b, x st o <> a & LIN (o,a,b) holds ex y st not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y))

    proof

      let o, a, b, x such that

       A1: o <> a and

       A2: LIN (o,a,b);

       A3:

      now

        consider p such that

         A4: not LIN (o,a,p) by A1, AFF_1: 13;

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

        o <> p by A4, AFF_1: 7;

        then

         A5: K is being_line by AFF_1:def 3;

        set A = ( Line (a,p));

        a <> p by A4, AFF_1: 7;

        then A is being_line by AFF_1:def 3;

        then

        consider B9 such that

         A6: b in B9 and

         A7: A // B9 by AFF_1: 49;

        

         A8: B9 is being_line by A7, AFF_1: 36;

        

         A9: a in A by AFF_1: 15;

        

         A10: p in K by AFF_1: 15;

        

         A11: p in A by AFF_1: 15;

        

         A12: o in K by AFF_1: 15;

         not B9 // K

        proof

          assume B9 // K;

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

          then A = K by A10, A11, AFF_1: 45;

          hence contradiction by A4, A12, A10, A9, A5, AFF_1: 21;

        end;

        then

        consider p9 such that

         A13: p9 in B9 and

         A14: p9 in K by A5, A8, AFF_1: 58;

        

         A15: (a,p) // (b,p9) by A9, A11, A6, A7, A13, AFF_1: 39;

        set M = ( Line (o,a));

        

         A16: o in M by AFF_1: 15;

        o <> a by A4, AFF_1: 7;

        then

         A17: M is being_line by AFF_1:def 3;

        set C = ( Line (p,x));

        assume

         A18: LIN (o,a,x);

        then

         A19: C is being_line by A4, AFF_1:def 3;

        then

        consider D such that

         A20: p9 in D and

         A21: C // D by AFF_1: 49;

        

         A22: p in C by AFF_1: 15;

        

         A23: LIN (o,p,p9) by A12, A10, A5, A14, AFF_1: 21;

        

         A24: a in M by AFF_1: 15;

        

         A25: x in C by AFF_1: 15;

        

         A26: x in M by A18, AFF_1:def 2;

        

         A27: not D // M

        proof

          assume D // M;

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

          then C = M by A26, A25, AFF_1: 45;

          hence contradiction by A4, A16, A24, A22, A19, AFF_1: 21;

        end;

        D is being_line by A21, AFF_1: 36;

        then

        consider y such that

         A28: y in D and

         A29: y in M by A17, A27, AFF_1: 58;

        

         A30: LIN (o,a,y) by A16, A24, A17, A29, AFF_1: 21;

        (p,x) // (p9,y) by A22, A25, A20, A21, A28, AFF_1: 39;

        hence thesis by A18, A4, A23, A15, A30;

      end;

      now

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

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

        then

        consider y such that

         A31: (x,o) // (o,y) and

         A32: (x,a) // (b,y) by A1, DIRAF: 40;

        (o,x) // (o,y) by A31, AFF_1: 4;

        then

         A33: LIN (o,x,y) by AFF_1:def 1;

        assume

         A34: not LIN (o,a,x);

        (a,x) // (b,y) by A32, AFF_1: 4;

        hence thesis by A34, A33;

      end;

      hence thesis by A3;

    end;

    

     Lm9: for o, a, b, y st o <> a & o <> b & LIN (o,a,b) holds ex x st not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y))

    proof

      let o, a, b, y;

      assume that

       A1: o <> a and

       A2: o <> b and

       A3: LIN (o,a,b);

      

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

      then

      consider x such that

       A5: not LIN (o,b,y) & LIN (o,y,x) & (b,y) // (a,x) or ( LIN (o,b,y) & ex p, p9 st not LIN (o,b,p) & LIN (o,p,p9) & (b,p) // (a,p9) & (p,y) // (p9,x) & LIN (o,b,x)) by A2, Lm8;

       not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y)) by A1, A2, A4, A5, Lm6;

      hence thesis;

    end;

    

     Lm10: o <> a & a = b & ( not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y))) implies x = y

    proof

      assume that

       A1: o <> a and

       A2: a = b and

       A3: not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y));

       A4:

      now

        

         A5: LIN (o,x,x) by AFF_1: 7;

        

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

        assume that

         A7: LIN (o,a,x) and

         A8: x <> o;

        consider p, q such that

         A9: not LIN (o,a,p) and

         A10: LIN (o,p,q) and

         A11: (a,p) // (b,q) and

         A12: (p,x) // (q,y) and

         A13: LIN (o,a,y) by A3, A7;

        

         A14: LIN (o,p,p) by AFF_1: 7;

        

         A15: not LIN (o,p,x)

        proof

          assume LIN (o,p,x);

          then

           A16: LIN (o,x,p) by AFF_1: 6;

          

           A17: LIN (o,x,o) by AFF_1: 7;

           LIN (o,x,a) by A7, AFF_1: 6;

          hence contradiction by A8, A9, A17, A16, AFF_1: 8;

        end;

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

        then

         A18: LIN (o,x,y) by A1, A7, A13, AFF_1: 8;

        (a,p) // (a,p) by AFF_1: 2;

        then

         A19: (p,x) // (p,y) by A2, A9, A10, A11, A12, A6, A14, AFF_1: 56;

        (p,x) // (p,x) by AFF_1: 2;

        hence thesis by A14, A15, A18, A19, A5, AFF_1: 56;

      end;

      now

        

         A20: LIN (o,x,x) by AFF_1: 7;

        

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

        

         A22: (a,x) // (a,x) by AFF_1: 2;

        assume not LIN (o,a,x);

        hence thesis by A2, A3, A22, A21, A20, AFF_1: 56;

      end;

      hence thesis by A1, A3, A4, Lm7;

    end;

    

     Lm11: o <> a & LIN (o,a,b) & AFP is Desarguesian & LIN (o,a,x) & (ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y)) & (ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,r) & LIN (o,a,r)) implies y = r

    proof

      assume that

       A1: o <> a and

       A2: LIN (o,a,b) and

       A3: AFP is Desarguesian and

       A4: LIN (o,a,x) and

       A5: ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y) and

       A6: ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,r) & LIN (o,a,r);

      consider q, q9 such that

       A7: not LIN (o,a,q) and

       A8: LIN (o,q,q9) and

       A9: (a,q) // (b,q9) and

       A10: (q,x) // (q9,r) and

       A11: LIN (o,a,r) by A6;

      

       A12: o <> q by A7, AFF_1: 7;

      consider p, p9 such that

       A13: not LIN (o,a,p) and

       A14: LIN (o,p,p9) and

       A15: (a,p) // (b,p9) and

       A16: (p,x) // (p9,y) and

       A17: LIN (o,a,y) by A5;

      

       A18: a = x implies thesis

      proof

        

         A19: (q,a) // (q9,b) by A9, AFF_1: 4;

        

         A20: not LIN (o,q,a) by A7, AFF_1: 6;

        

         A21: (p,a) // (p9,b) by A15, AFF_1: 4;

        assume

         A22: a = x;

         not LIN (o,p,a) by A13, AFF_1: 6;

        then b = y by A2, A14, A16, A17, A22, A21, AFF_1: 56;

        hence thesis by A2, A8, A10, A11, A22, A20, A19, AFF_1: 56;

      end;

      

       A23: o <> p by A13, AFF_1: 7;

      

       A24: a <> b & a <> x & p <> q & o <> x implies thesis

      proof

        assume that a <> b and a <> x and

         A25: p <> q and

         A26: o <> x;

         A27:

        now

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

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

          

           A28: LIN (o,q,o) by AFF_1: 7;

          

           A29: o in A by AFF_1: 15;

          

           A30: p in K by AFF_1: 15;

          

           A31: o in K by AFF_1: 15;

          

           A32: A is being_line by A1, AFF_1:def 3;

          

           A33: x in A by A4, AFF_1:def 2;

          r in A by A11, AFF_1:def 2;

          then

           A34: LIN (o,x,r) by A32, A29, A33, AFF_1: 21;

          

           A35: (x,p) // (y,p9) by A16, AFF_1: 4;

          assume

           A36: LIN (o,p,q);

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

          then LIN (o,p,q9) by A8, A12, A28, AFF_1: 8;

          then (x,q) // (y,q9) by A2, A3, A4, A13, A14, A15, A17, A9, A12, A25, A26, A36, A35, Th1;

          then

           A37: (q,x) // (q9,y) by AFF_1: 4;

          

           A38: K is being_line by A23, AFF_1:def 3;

          

           A39: q in K by A36, AFF_1:def 2;

          

           A40: not LIN (o,q,x)

          proof

            assume

             A41: LIN (o,q,x);

            K = ( Line (o,q)) by A12, A38, A31, A39, AFF_1: 24;

            then x in K by A41, AFF_1:def 2;

            then

             A42: p in A by A26, A32, A29, A33, A38, A31, A30, AFF_1: 18;

            

             A43: a in A by AFF_1: 15;

            A is being_line by A1, AFF_1:def 3;

            hence contradiction by A13, A29, A43, A42, AFF_1: 21;

          end;

          y in A by A17, AFF_1:def 2;

          then LIN (o,x,y) by A32, A29, A33, AFF_1: 21;

          hence thesis by A8, A10, A37, A40, A34, AFF_1: 56;

        end;

        now

          

           A44: not LIN (o,p,x)

          proof

            assume LIN (o,p,x);

            then

             A45: LIN (o,x,p) by AFF_1: 6;

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

            hence contradiction by A4, A13, A26, A45, AFF_1: 11;

          end;

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

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

          assume

           A46: not LIN (o,p,q);

          

           A47: o in A by AFF_1: 15;

          

           A48: q in K by AFF_1: 15;

          

           A49: o in K by AFF_1: 15;

          

           A50: A is being_line by A1, AFF_1:def 3;

          

           A51: x in A by A4, AFF_1:def 2;

          

           A52: y in A by A17, AFF_1:def 2;

          then

           A53: LIN (o,x,y) by A50, A47, A51, AFF_1: 21;

          

           A54: K is being_line by A12, AFF_1:def 3;

          

           A55: not LIN (o,q,x)

          proof

            assume LIN (o,q,x);

            then x in K by AFF_1:def 2;

            then

             A56: q in A by A26, A50, A47, A51, A54, A49, A48, AFF_1: 18;

            

             A57: a in A by AFF_1: 15;

            A is being_line by A1, AFF_1:def 3;

            hence contradiction by A7, A47, A57, A56, AFF_1: 21;

          end;

          r in A by A11, AFF_1:def 2;

          then

           A58: LIN (o,x,r) by A50, A47, A51, AFF_1: 21;

          

           A59: LIN (o,x,y) by A50, A47, A51, A52, AFF_1: 21;

          (p,q) // (p9,q9) by A2, A3, A13, A14, A15, A7, A8, A9, Lm1;

          then (q,x) // (q9,y) by A3, A14, A16, A8, A46, A44, A53, Lm1;

          hence thesis by A8, A10, A55, A59, A58, AFF_1: 56;

        end;

        hence thesis by A27;

      end;

      

       A60: o <> a by A13, AFF_1: 7;

      

       A61: p = q & o <> x implies thesis

      proof

        assume that

         A62: p = q and

         A63: o <> x;

        

         A64: not LIN (o,p,x)

        proof

          assume LIN (o,p,x);

          then

           A65: LIN (o,x,p) by AFF_1: 6;

          

           A66: LIN (o,x,o) by AFF_1: 7;

           LIN (o,x,a) by A4, AFF_1: 6;

          hence contradiction by A13, A63, A66, A65, AFF_1: 8;

        end;

        

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

        then

         A68: LIN (o,x,y) by A4, A17, A60, AFF_1: 8;

        

         A69: LIN (o,x,r) by A4, A11, A60, A67, AFF_1: 8;

        p9 = q9 by A2, A13, A14, A15, A8, A9, A62, AFF_1: 56;

        hence thesis by A14, A16, A10, A62, A68, A69, A64, AFF_1: 56;

      end;

      

       A70: o = x implies thesis

      proof

        assume

         A71: o = x;

        then y = o by A1, A4, A5, Lm7;

        hence thesis by A1, A4, A6, A71, Lm7;

      end;

      a = b implies thesis

      proof

        assume

         A72: a = b;

        then x = y by A1, A4, A5, Lm10;

        hence thesis by A1, A4, A6, A72, Lm10;

      end;

      hence thesis by A70, A61, A18, A24;

    end;

    

     Lm12: o <> a & o <> b & LIN (o,a,b) & AFP is Desarguesian & ( not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y))) & ( not LIN (o,a,r) & LIN (o,r,y) & (a,r) // (b,y) or ( LIN (o,a,r) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,r) // (p9,y) & LIN (o,a,y))) implies x = r

    proof

      assume that

       A1: o <> a and

       A2: o <> b and

       A3: LIN (o,a,b) and

       A4: AFP is Desarguesian and

       A5: not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y)) and

       A6: not LIN (o,a,r) & LIN (o,r,y) & (a,r) // (b,y) or ( LIN (o,a,r) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,r) // (p9,y) & LIN (o,a,y));

      

       A7: not LIN (o,b,y) & LIN (o,y,r) & (b,y) // (a,r) or ( LIN (o,b,y) & ex p, p9 st not LIN (o,b,p) & LIN (o,p,p9) & (b,p) // (a,p9) & (p,y) // (p9,r) & LIN (o,b,r)) by A1, A2, A3, A6, Lm6;

      

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

       not LIN (o,b,y) & LIN (o,y,x) & (b,y) // (a,x) or ( LIN (o,b,y) & ex p, p9 st not LIN (o,b,p) & LIN (o,p,p9) & (b,p) // (a,p9) & (p,y) // (p9,x) & LIN (o,b,x)) by A1, A2, A3, A5, Lm6;

      hence thesis by A2, A4, A8, A7, Lm11, AFF_1: 56;

    end;

    

     Lm13: for o, a, b st AFP is Desarguesian & o <> a & o <> b & LIN (o,a,b) holds ex f st for x, y holds ((f . x) = y iff ( not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y))))

    proof

      let o, a, b;

      defpred P[ Element of AFP, Element of AFP] means (( not LIN (o,a,$1) & LIN (o,$1,$2) & (a,$1) // (b,$2)) or ( LIN (o,a,$1) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,$1) // (p9,$2) & LIN (o,a,$2)));

      assume that

       A1: AFP is Desarguesian and

       A2: o <> a and

       A3: o <> b and

       A4: LIN (o,a,b);

      

       A5: for y holds ex x st P[x, y] by A2, A3, A4, Lm9;

      

       A6: for x holds ex y st P[x, y] by A2, A4, Lm8;

      

       A7: for x, y, s st P[x, y] & P[x, s] holds y = s by A1, A2, A4, Lm11, AFF_1: 56;

      

       A8: for x, y, r st P[x, y] & P[r, y] holds x = r by A1, A2, A3, A4, Lm12;

      ex f st for x, y holds ((f . x) = y iff P[x, y]) from TRANSGEO:sch 1( A6, A5, A8, A7);

      hence thesis;

    end;

    

     Lm14: AFP is Desarguesian & o <> a & LIN (o,a,b) & not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) & LIN (o,a,z) & (ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,z) // (p9,t) & LIN (o,a,t)) implies (x,z) // (y,t)

    proof

      assume that

       A1: AFP is Desarguesian and

       A2: o <> a and

       A3: LIN (o,a,b) and

       A4: not LIN (o,a,x) and

       A5: LIN (o,x,y) and

       A6: (a,x) // (b,y) and

       A7: LIN (o,a,z) and

       A8: ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,z) // (p9,t) & LIN (o,a,t);

      consider p, p9 such that

       A9: not LIN (o,a,p) and

       A10: LIN (o,p,p9) and

       A11: (a,p) // (b,p9) and

       A12: (p,z) // (p9,t) and

       A13: LIN (o,a,t) by A8;

       A14:

      now

        

         A15: (p,a) // (p9,b) by A11, AFF_1: 4;

        assume

         A16: a = z;

         not LIN (o,p,a) by A9, AFF_1: 6;

        then (z,x) // (t,y) by A3, A6, A10, A12, A13, A16, A15, AFF_1: 56;

        hence thesis by AFF_1: 4;

      end;

      

       A17: (p,x) // (p9,y) by A1, A3, A4, A5, A6, A9, A10, A11, Lm1;

       A18:

      now

        assume that

         A19: z <> o and

         A20: not LIN (o,p,x);

        

         A21: not LIN (o,p,z)

        proof

          

           A22: LIN (o,p,o) by AFF_1: 7;

          assume

           A23: LIN (o,p,z);

           LIN (o,z,a) by A7, AFF_1: 6;

          then LIN (o,p,a) by A19, A23, A22, AFF_1: 11;

          hence contradiction by A9, AFF_1: 6;

        end;

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

        then LIN (o,z,t) by A2, A7, A13, AFF_1: 8;

        hence thesis by A1, A5, A10, A12, A17, A20, A21, Lm1;

      end;

      

       A24: o <> x by A4, AFF_1: 7;

       A25:

      now

        assume that

         A26: z <> o and

         A27: LIN (o,p,x) and a <> z;

        now

          

           A28: LIN (o,x,o) by AFF_1: 7;

           LIN (o,x,p) by A27, AFF_1: 6;

          then

           A29: LIN (o,p,y) by A5, A24, A28, AFF_1: 8;

          assume

           A30: x <> p;

          (z,p) // (t,p9) by A12, AFF_1: 4;

          then (z,x) // (t,y) by A1, A3, A6, A7, A9, A10, A11, A13, A24, A26, A27, A30, A29, Th1;

          hence thesis by AFF_1: 4;

        end;

        hence thesis by A3, A4, A5, A6, A10, A11, A12, AFF_1: 56;

      end;

      now

        

         A31: (o,x) // (o,y) by A5, AFF_1:def 1;

        assume

         A32: z = o;

        then t = o by A2, A7, A8, Lm7;

        hence thesis by A32, A31, AFF_1: 4;

      end;

      hence thesis by A18, A14, A25;

    end;

    

     Lm15: AFP is Desarguesian & o <> a & LIN (o,a,b) & LIN (o,a,x) & (ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y)) & not LIN (o,a,z) & LIN (o,z,t) & (a,z) // (b,t) implies (x,z) // (y,t)

    proof

      assume that

       A1: AFP is Desarguesian and

       A2: o <> a and

       A3: LIN (o,a,b) and

       A4: LIN (o,a,x) and

       A5: ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y) and

       A6: not LIN (o,a,z) and

       A7: LIN (o,z,t) and

       A8: (a,z) // (b,t);

      (z,x) // (t,y) by A1, A2, A3, A4, A5, A6, A7, A8, Lm14;

      hence thesis by AFF_1: 4;

    end;

    

     Lm16: o <> a & LIN (o,a,x) & (ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y)) & LIN (o,a,z) & (ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,z) // (p9,t) & LIN (o,a,t)) implies (x,z) // (y,t)

    proof

      assume that

       A1: o <> a and

       A2: LIN (o,a,x) and

       A3: ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y) and

       A4: LIN (o,a,z) and

       A5: ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,z) // (p9,t) & LIN (o,a,t);

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

      

       A6: x in A by A2, AFF_1:def 2;

      

       A7: z in A by A4, AFF_1:def 2;

      

       A8: y in A by A3, AFF_1:def 2;

      

       A9: t in A by A5, AFF_1:def 2;

      

       A10: A is being_line by A1, AFF_1:def 3;

      now

        assume

         A11: x <> z;

        then A = ( Line (x,z)) by A10, A6, A7, AFF_1: 24;

        hence thesis by A8, A9, A11, AFF_1: 22;

      end;

      hence thesis by AFF_1: 3;

    end;

    

     Lm17: o <> a & LIN (o,a,b) & AFP is Desarguesian & (for x, y holds ((f . x) = y iff (( not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y)) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y))))) implies f is dilatation & (f . o) = o & (f . a) = b

    proof

      assume that

       A1: o <> a and

       A2: LIN (o,a,b) and

       A3: AFP is Desarguesian;

      assume

       A4: for x, y holds ((f . x) = y iff ( not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y))));

      for x, r holds (x,r) // ((f . x),(f . r))

      proof

        let x, r;

        set y = (f . x);

        set s = (f . r);

        

         A5: not LIN (o,a,r) & LIN (o,r,s) & (a,r) // (b,s) or ( LIN (o,a,r) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,r) // (p9,s) & LIN (o,a,s)) by A4;

         not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y)) by A4;

        hence thesis by A1, A2, A3, A5, Lm1, Lm14, Lm15, Lm16;

      end;

      hence f is dilatation by TRANSGEO: 68;

      thus (f . o) = o

      proof

        set y = (f . o);

         not LIN (o,a,o) & LIN (o,o,y) & (a,o) // (b,y) or ( LIN (o,a,o) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,o) // (p9,y) & LIN (o,a,y)) by A4;

        hence thesis by A1, Lm7;

      end;

      thus (f . a) = b

      proof

        set y = (f . a);

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

        then

        consider p, p9 such that

         A6: not LIN (o,a,p) and

         A7: LIN (o,p,p9) and

         A8: (a,p) // (b,p9) and

         A9: (p,a) // (p9,y) and

         A10: LIN (o,a,y) by A4;

        

         A11: (p,a) // (p9,b) by A8, AFF_1: 4;

         not LIN (o,p,a) by A6, AFF_1: 6;

        hence thesis by A2, A7, A9, A10, A11, AFF_1: 56;

      end;

    end;

    theorem :: HOMOTHET:3

    

     Th3: AFP is Desarguesian implies for o, a, b st o <> a & o <> b & LIN (o,a,b) holds ex f st f is dilatation & (f . o) = o & (f . a) = b

    proof

      assume

       A1: AFP is Desarguesian;

      let o, a, b;

      assume that

       A2: o <> a and

       A3: o <> b and

       A4: LIN (o,a,b);

      consider f such that

       A5: for x, y holds ((f . x) = y iff ( not LIN (o,a,x) & LIN (o,x,y) & (a,x) // (b,y) or ( LIN (o,a,x) & ex p, p9 st not LIN (o,a,p) & LIN (o,p,p9) & (a,p) // (b,p9) & (p,x) // (p9,y) & LIN (o,a,y)))) by A1, A2, A3, A4, Lm13;

      

       A6: (f . a) = b by A1, A2, A4, A5, Lm17;

      

       A7: (f . o) = o by A1, A2, A4, A5, Lm17;

      f is dilatation by A1, A2, A4, A5, Lm17;

      hence thesis by A7, A6;

    end;

    theorem :: HOMOTHET:4

    AFP is Desarguesian iff for o, a, b st o <> a & o <> b & LIN (o,a,b) holds ex f st f is dilatation & (f . o) = o & (f . a) = b by Th2, Th3;

    definition

      let AFP, f, K;

      :: HOMOTHET:def1

      pred f is_Sc K means f is collineation & K is being_line & (for x st x in K holds (f . x) = x) & for x holds (x,(f . x)) // K;

    end

    theorem :: HOMOTHET:5

    

     Th5: f is_Sc K & (f . p) = p & not p in K implies f = ( id the carrier of AFP) by TRANSGEO: 97;

    theorem :: HOMOTHET:6

    

     Th6: (for a, b, K st (a,b) // K & not a in K holds ex f st f is_Sc K & (f . a) = b) implies AFP is Moufangian

    proof

      assume

       A1: for a, b, K st (a,b) // K & not a in K holds ex f st f is_Sc K & (f . a) = b;

      now

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

        assume that

         A2: o in K and

         A3: c in K and

         A4: c9 in K and

         A5: K is being_line and

         A6: LIN (o,a,a9) and

         A7: LIN (o,b,b9) and

         A8: not a in K and

         A9: (a,b) // K and

         A10: (a9,b9) // K and

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

        consider f such that

         A12: f is_Sc K and

         A13: (f . a) = b by A1, A8, A9;

        

         A14: f is collineation by A12;

        

         A15: (a,b) // (a9,b9) by A5, A9, A10, AFF_1: 31;

        

         A16: (f . a9) = b9

        proof

          set x = (f . a9);

           A17:

          now

            (f . o) = o by A2, A12;

            then

             A18: LIN (o,b,x) by A6, A13, A14, TRANSGEO: 88;

            (a9,x) // K by A12;

            then

             A19: (a,b) // (a9,x) by A5, A9, AFF_1: 31;

            assume a <> b;

            hence thesis by A2, A6, A7, A8, A9, A15, A19, A18, AFF_1: 46, AFF_1: 56;

          end;

          now

            assume

             A20: a = b;

            then f = ( id the carrier of AFP) by A8, A12, A13, Th5;

            then x = a9 by FUNCT_1: 18;

            hence thesis by A2, A6, A7, A8, A10, A20, AFF_1: 47;

          end;

          hence thesis by A17;

        end;

        

         A21: (f . c9) = c9 by A4, A12;

        (f . c) = c by A3, A12;

        hence (b,c) // (b9,c9) by A11, A13, A14, A21, A16, TRANSGEO: 87;

      end;

      hence thesis by Lm2;

    end;

    

     Lm18: (a,b) // K & not a in K & (x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K)) implies (b,a) // K & not b in K & (y in K & y = x or ( not y in K & ex p, p9 st p in K & p9 in K & (p,b) // (p9,y) & (p,a) // (p9,x) & (y,x) // K)) by AFF_1: 34, AFF_1: 35;

    

     Lm19: (a,b) // K & not a in K implies for x holds ex y st (x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K))

    proof

      assume that

       A1: (a,b) // K and

       A2: not a in K;

      

       A3: not b in K by A1, A2, AFF_1: 35;

      

       A4: K is being_line by A1, AFF_1: 26;

      let x;

      consider p, q such that

       A5: p in K and q in K and p <> q by A1, AFF_1: 19, AFF_1: 26;

      

       A6: p <> b by A1, A2, A5, AFF_1: 35;

      now

        set B9 = ( Line (p,b));

        set A = ( Line (p,a));

        assume

         A7: not x in K;

        

         A8: a in A by AFF_1: 15;

        A is being_line by A2, A5, AFF_1:def 3;

        then

        consider C such that

         A9: x in C and

         A10: A // C by AFF_1: 49;

        

         A11: C is being_line by A10, AFF_1: 36;

        

         A12: p in A by AFF_1: 15;

        then not A // K by A2, A5, A8, AFF_1: 45;

        then not C // K by A10, AFF_1: 44;

        then

        consider p9 such that

         A13: p9 in C and

         A14: p9 in K by A4, A11, AFF_1: 58;

        B9 is being_line by A6, AFF_1:def 3;

        then

        consider D such that

         A15: p9 in D and

         A16: B9 // D by AFF_1: 49;

        

         A17: b in B9 by AFF_1: 15;

        K is being_line by A1, AFF_1: 26;

        then

        consider M such that

         A18: x in M and

         A19: K // M by AFF_1: 49;

        

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

        

         A21: p in B9 by AFF_1: 15;

        then

         A22: not B9 // K by A5, A3, A17, AFF_1: 45;

        

         A23: not D // M

        proof

          assume D // M;

          then B9 // M by A16, AFF_1: 44;

          hence contradiction by A22, A19, AFF_1: 44;

        end;

        D is being_line by A16, AFF_1: 36;

        then

        consider y such that

         A24: y in D and

         A25: y in M by A20, A23, AFF_1: 58;

        

         A26: (p,b) // (p9,y) by A21, A17, A15, A16, A24, AFF_1: 39;

        

         A27: (x,y) // K by A18, A19, A25, AFF_1: 40;

        (p,a) // (p9,x) by A12, A8, A9, A10, A13, AFF_1: 39;

        hence thesis by A5, A7, A14, A27, A26;

      end;

      hence thesis;

    end;

    

     Lm20: (a,b) // K & not a in K implies for y holds ex x st (x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K))

    proof

      assume that

       A1: (a,b) // K and

       A2: not a in K;

      let y;

      

       A3: (b,a) // K by A1, AFF_1: 34;

      

       A4: not b in K by A1, A2, AFF_1: 35;

      then

      consider x such that

       A5: y in K & y = x or ( not y in K & ex p, p9 st p in K & p9 in K & (p,b) // (p9,y) & (p,a) // (p9,x) & (y,x) // K) by A3, Lm19;

      x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K) by A3, A4, A5, Lm18;

      hence thesis;

    end;

    theorem :: HOMOTHET:7

    

     Th7: K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian & a in M & b in M & x in M & y in M & a <> b & q <> p & (p,a) // (p9,x) & (p,b) // (p9,y) & (q,a) // (q9,x) implies (q,b) // (q9,y)

    proof

      assume that

       A1: K // M and

       A2: p in K and

       A3: q in K and

       A4: p9 in K and

       A5: q9 in K and

       A6: AFP is Moufangian and

       A7: a in M and

       A8: b in M and

       A9: x in M and

       A10: y in M and

       A11: a <> b and

       A12: q <> p and

       A13: (p,a) // (p9,x) and

       A14: (p,b) // (p9,y) and

       A15: (q,a) // (q9,x);

      

       A16: K is being_line by A1, AFF_1: 36;

      

       A17: M is being_line by A1, AFF_1: 36;

      now

        set D9 = ( Line (q9,x));

        set B99 = ( Line (p9,y));

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

        set B9 = ( Line (p,b));

        

         A18: q in D by AFF_1: 15;

        

         A19: a in D by AFF_1: 15;

        

         A20: x in D9 by AFF_1: 15;

        

         A21: q9 in D9 by AFF_1: 15;

        

         A22: LIN (p,q,q9) by A2, A3, A5, A16, AFF_1: 21;

        

         A23: LIN (p,q,p9) by A2, A3, A4, A16, AFF_1: 21;

        assume

         A24: K <> M;

        then

         A25: q9 <> x by A1, A5, A9, AFF_1: 45;

        

         A26: not a in K by A1, A7, A24, AFF_1: 45;

        

         A27: b <> p by A1, A2, A8, A24, AFF_1: 45;

        then

         A28: B9 is being_line by AFF_1:def 3;

        

         A29: not q in M by A1, A3, A24, AFF_1: 45;

        

         A30: not p in M by A1, A2, A24, AFF_1: 45;

        

         A31: LIN (a,b,x) by A7, A8, A9, A17, AFF_1: 21;

         A32:

        now

           A33:

          now

            assume that

             A34: q = p9 and

             A35: q = q9;

             LIN (q,a,x) by A15, A35, AFF_1:def 1;

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

            then a = x by A7, A9, A17, A29, AFF_1: 25;

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

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

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

            hence contradiction by A2, A3, A12, A16, A26, AFF_1: 25;

          end;

           A36:

          now

            assume that

             A37: p = p9 and

             A38: p = q9;

             LIN (p,a,x) by A13, A37, AFF_1:def 1;

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

            then a = x by A7, A9, A17, A30, AFF_1: 25;

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

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

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

            hence contradiction by A2, A3, A12, A16, A26, AFF_1: 25;

          end;

          assume

           A39: not ex a, b, c st LIN (a,b,c) & a <> b & a <> c & b <> c;

           A40:

          now

            assume that

             A41: q = p9 and

             A42: p = q9;

             A43:

            now

              assume

               A44: b = x;

              then (q,y) // (q,a) by A14, A15, A27, A41, A42, AFF_1: 5;

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

              then LIN (a,y,q) by AFF_1: 6;

              then (q9,y) // (q,b) by A7, A10, A13, A17, A29, A41, A42, A44, AFF_1: 25;

              hence thesis by AFF_1: 4;

            end;

            now

              assume a = x;

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

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

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

              hence contradiction by A2, A3, A12, A16, A26, AFF_1: 25;

            end;

            hence thesis by A11, A31, A39, A43;

          end;

          now

            assume that

             A45: p = p9 and

             A46: q = q9;

             LIN (p,b,y) by A14, A45, AFF_1:def 1;

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

            then b = y by A8, A10, A17, A30, AFF_1: 25;

            hence thesis by A46, AFF_1: 2;

          end;

          hence thesis by A12, A23, A22, A39, A36, A33, A40;

        end;

        

         A47: y in B99 by AFF_1: 15;

        

         A48: p9 in B99 by AFF_1: 15;

        

         A49: b in B9 by AFF_1: 15;

        then

         A50: B9 <> K by A1, A8, A24, AFF_1: 45;

        a <> q by A1, A3, A7, A24, AFF_1: 45;

        then

         A51: D // D9 by A15, A25, AFF_1: 37;

        

         A52: p in B9 by AFF_1: 15;

        then

         A53: B9 <> M by A1, A2, A24, AFF_1: 45;

        

         A54: p9 <> y by A1, A4, A10, A24, AFF_1: 45;

        then

         A55: B9 // B99 by A14, A27, AFF_1: 37;

        

         A56: B99 is being_line by A54, AFF_1:def 3;

        now

          

           A57: (a,q) // (x,q9) by A18, A19, A21, A20, A51, AFF_1: 39;

          assume ex a, b, c st LIN (a,b,c) & a <> b & a <> c & b <> c;

          then

          consider d such that

           A58: LIN (p,b,d) and

           A59: d <> p and

           A60: d <> b by TRANSLAC: 1;

          consider N such that

           A61: d in N and

           A62: K // N by A16, AFF_1: 49;

          

           A63: d in B9 by A58, AFF_1:def 2;

          then

           A64: N <> M by A8, A17, A28, A49, A53, A60, A61, AFF_1: 18;

          

           A65: not B99 // N

          proof

            assume B99 // N;

            then B9 // N by A55, AFF_1: 44;

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

            hence contradiction by A2, A52, A50, AFF_1: 45;

          end;

          N is being_line by A62, AFF_1: 36;

          then

          consider z such that

           A66: z in B99 and

           A67: z in N by A56, A65, AFF_1: 58;

          

           A68: (d,b) // (z,y) by A49, A47, A55, A63, A66, AFF_1: 39;

          

           A69: N <> K by A2, A16, A28, A52, A50, A59, A63, A61, AFF_1: 18;

          

           A70: M // N by A1, A62, AFF_1: 44;

          

           A71: K <> N by A2, A16, A28, A52, A50, A59, A63, A61, AFF_1: 18;

          

           A72: N // M by A1, A62, AFF_1: 44;

          (p,d) // (p9,z) by A52, A48, A55, A63, A66, AFF_1: 39;

          then

           A73: (a,d) // (x,z) by A1, A2, A4, A6, A7, A9, A13, A24, A61, A62, A67, A71, Lm4;

          M <> N by A8, A17, A28, A49, A53, A60, A63, A61, AFF_1: 18;

          then (d,q) // (z,q9) by A1, A3, A5, A6, A7, A9, A24, A61, A67, A73, A57, A70, Lm4;

          hence thesis by A3, A5, A6, A8, A10, A61, A62, A67, A68, A72, A64, A69, Lm4;

        end;

        hence thesis by A32;

      end;

      hence thesis by A1, A3, A5, A8, A10, AFF_1: 39;

    end;

    

     Lm21: (a,b) // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K & q in K & q9 in K & (q,a) // (q9,x) implies (q,b) // (q9,y)

    proof

      assume that

       A1: (a,b) // K and

       A2: not a in K and

       A3: not x in K and

       A4: AFP is Moufangian and

       A5: p in K and

       A6: p9 in K and

       A7: (p,a) // (p9,x) and

       A8: (p,b) // (p9,y) and

       A9: (x,y) // K and

       A10: q in K and

       A11: q9 in K and

       A12: (q,a) // (q9,x);

      

       A13: K is being_line by A1, AFF_1: 26;

       A14:

      now

        

         A15: (a,q) // (x,q9) by A12, AFF_1: 4;

        

         A16: (b,p) // (y,p9) by A8, AFF_1: 4;

        

         A17: (a,p) // (x,p9) by A7, AFF_1: 4;

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

        assume that

         A18: not (a,x) // K and

         A19: a <> b;

        a <> x by A13, A18, AFF_1: 33;

        then

         A20: A is being_line by AFF_1:def 3;

        

         A21: x in A by AFF_1: 15;

        

         A22: a in A by AFF_1: 15;

        then

        consider o such that

         A23: o in A and

         A24: o in K by A13, A18, A21, A20, AFF_1: 40, AFF_1: 58;

        

         A25: LIN (o,a,x) by A22, A21, A20, A23, AFF_1: 21;

        K is being_line by A1, AFF_1: 26;

        then (a,b) // (x,y) by A1, A9, AFF_1: 31;

        then LIN (o,b,y) by A1, A2, A4, A5, A6, A19, A24, A25, A17, A16, Lm3, AFF_1: 26;

        then (b,q) // (y,q9) by A1, A2, A4, A9, A10, A11, A13, A24, A25, A15, Lm2;

        hence thesis by AFF_1: 4;

      end;

       A26:

      now

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

        assume that

         A27: (a,x) // K and

         A28: a <> b and

         A29: p <> q;

        

         A30: M is being_line by A28, AFF_1:def 3;

        K is being_line by A1, AFF_1: 26;

        then (a,b) // (a,x) by A1, A27, AFF_1: 31;

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

        then

         A31: x in M by AFF_1:def 2;

        

         A32: b in M by AFF_1: 15;

        

         A33: a in M by AFF_1: 15;

        

         A34: M // K by A1, A28, AFF_1:def 5;

        then (x,y) // M by A9, AFF_1: 43;

        then y in M by A30, A31, AFF_1: 23;

        hence thesis by A4, A5, A6, A7, A8, A10, A11, A12, A28, A29, A33, A32, A34, A31, Th7;

      end;

      

       A35: a = b implies x = y

      proof

        set M = ( Line (x,y));

        

         A36: x in M by AFF_1: 15;

        assume a = b;

        then (p9,x) // (p9,y) by A2, A5, A7, A8, AFF_1: 5;

        then LIN (p9,x,y) by AFF_1:def 1;

        then LIN (x,y,p9) by AFF_1: 6;

        then

         A37: p9 in M by AFF_1:def 2;

        assume x <> y;

        then M // K by A9, AFF_1:def 5;

        hence contradiction by A3, A6, A36, A37, AFF_1: 45;

      end;

      now

        assume

         A38: p = q;

        p9 = q9

        proof

          (p9,x) // (q9,x) by A2, A5, A7, A12, A38, AFF_1: 5;

          then (x,p9) // (x,q9) by AFF_1: 4;

          then LIN (x,p9,q9) by AFF_1:def 1;

          then

           A39: LIN (p9,q9,x) by AFF_1: 6;

          assume p9 <> q9;

          hence contradiction by A1, A3, A6, A11, A39, AFF_1: 25, AFF_1: 26;

        end;

        hence thesis by A8, A38;

      end;

      hence thesis by A12, A35, A14, A26;

    end;

    

     Lm22: (a,b) // K & not a in K & not x in K & AFP is Moufangian & p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K & q in K & q9 in K & (q,a) // (q9,x) & (x,s) // K & (q,b) // (q9,s) implies s = y

    proof

      assume that

       A1: (a,b) // K and

       A2: not a in K and

       A3: not x in K and

       A4: AFP is Moufangian and

       A5: p in K and

       A6: p9 in K and

       A7: (p,a) // (p9,x) and

       A8: (p,b) // (p9,y) and

       A9: (x,y) // K and

       A10: q in K and

       A11: q9 in K and

       A12: (q,a) // (q9,x) and

       A13: (x,s) // K and

       A14: (q,b) // (q9,s);

      

       A15: not b in K by A1, A2, AFF_1: 35;

      (q,b) // (q9,y) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, Lm21;

      then (q9,s) // (q9,y) by A10, A14, A15, AFF_1: 5;

      then LIN (q9,s,y) by AFF_1:def 1;

      then

       A16: LIN (y,s,q9) by AFF_1: 6;

      assume

       A17: not thesis;

      K is being_line by A1, AFF_1: 26;

      then

      consider M such that

       A18: x in M and

       A19: K // M by AFF_1: 49;

      

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

      (x,s) // M by A13, A19, AFF_1: 43;

      then

       A21: s in M by A18, A20, AFF_1: 23;

      (x,y) // M by A9, A19, AFF_1: 43;

      then y in M by A18, A20, AFF_1: 23;

      then M = ( Line (y,s)) by A17, A20, A21, AFF_1: 24;

      then q9 in M by A16, AFF_1:def 2;

      hence contradiction by A3, A11, A18, A19, AFF_1: 45;

    end;

    

     Lm23: (a,b) // K & not a in K & AFP is Moufangian & (x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K)) & (r in K & r = y or ( not r in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,r) & (p,b) // (p9,y) & (r,y) // K)) implies x = r

    proof

      assume that

       A1: (a,b) // K and

       A2: not a in K and

       A3: AFP is Moufangian and

       A4: x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K) and

       A5: r in K & r = y or ( not r in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,r) & (p,b) // (p9,y) & (r,y) // K);

      

       A6: y in K & y = r or ( not y in K & ex p, p9 st p in K & p9 in K & (p,b) // (p9,y) & (p,a) // (p9,r) & (y,r) // K) by A1, A2, A5, Lm18;

      

       A7: (b,a) // K by A1, AFF_1: 34;

      

       A8: not b in K by A1, A2, AFF_1: 35;

      y in K & y = x or ( not y in K & ex p, p9 st p in K & p9 in K & (p,b) // (p9,y) & (p,a) // (p9,x) & (y,x) // K) by A1, A2, A4, Lm18;

      hence thesis by A3, A7, A8, A6, Lm22;

    end;

    

     Lm24: (a,b) // K & not a in K & AFP is Moufangian implies ex f st for x, y holds ((f . x) = y iff (x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K)))

    proof

      defpred P[ Element of AFP, Element of AFP] means (($1 in K & $1 = $2) or ( not $1 in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,$1) & (p,b) // (p9,$2) & ($1,$2) // K));

      assume that

       A1: (a,b) // K and

       A2: not a in K and

       A3: AFP is Moufangian;

      

       A4: for x, y, s st P[x, y] & P[x, s] holds y = s by A1, A2, A3, Lm22;

      

       A5: for y holds ex x st P[x, y] by A1, A2, Lm20;

      

       A6: for x holds ex y st P[x, y] by A1, A2, Lm19;

      

       A7: for x, y, r st P[x, y] & P[r, y] holds x = r by A1, A2, A3, Lm23;

      ex f st for x, y holds ((f . x) = y iff P[x, y]) from TRANSGEO:sch 1( A6, A5, A7, A4);

      hence thesis;

    end;

    

     Lm25: ((a,b) // K & not a in K & for x, y holds ((f . x) = y iff (x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K)))) implies (f . a) = b

    proof

      assume that

       A1: (a,b) // K and

       A2: not a in K;

      consider p, q such that

       A3: p in K and q in K and p <> q by A1, AFF_1: 19, AFF_1: 26;

      

       A4: (p,b) // (p,b) by AFF_1: 2;

      assume

       A5: for x, y holds ((f . x) = y iff (x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K)));

      (p,a) // (p,a) by AFF_1: 2;

      hence thesis by A1, A2, A5, A3, A4;

    end;

    

     Lm26: ((a,b) // K & for x, y holds ((f . x) = y iff (x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K)))) implies for x holds (x,(f . x)) // K

    proof

      assume that

       A1: (a,b) // K and

       A2: for x, y holds ((f . x) = y iff (x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K)));

      let x;

      set y = (f . x);

      

       A3: K is being_line by A1, AFF_1: 26;

       A4:

      now

        assume x in K;

        then y = x by A2;

        hence thesis by A3, AFF_1: 33;

      end;

      now

        assume not x in K;

        then ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K by A2;

        hence thesis;

      end;

      hence thesis by A4;

    end;

    

     Lm27: ((a,b) // K & not a in K & for x, y holds ((f . x) = y iff (x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K)))) implies f is collineation

    proof

      assume that

       A1: (a,b) // K and

       A2: not a in K and

       A3: for x, y holds ((f . x) = y iff (x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K)));

      

       A4: K is being_line by A1, AFF_1: 26;

      

       A5: not b in K by A1, A2, AFF_1: 35;

      for A st A is being_line holds (f .: A) is being_line

      proof

        let A such that

         A6: A is being_line;

        set B9 = (f .: A);

         A7:

        now

          assume that

           A8: A // K and

           A9: A <> K;

          now

            let x such that

             A10: x in A;

            consider y such that

             A11: (f . y) = x by TRANSGEO: 1;

            y in K & y = x or ( not y in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,y) & (p,b) // (p9,x) & (y,x) // K) by A3, A11;

            then (x,y) // K by A8, A9, A10, AFF_1: 34, AFF_1: 45;

            then (x,y) // A by A8, AFF_1: 43;

            then y in A by A6, A10, AFF_1: 23;

            hence x in B9 by A11, TRANSGEO: 91;

          end;

          then

           A12: A c= B9 by SUBSET_1: 2;

          now

            let y;

            assume y in B9;

            then

            consider x such that

             A13: x in A and

             A14: y = (f . x) by TRANSGEO: 91;

             not x in K by A8, A9, A13, AFF_1: 45;

            then ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K by A3, A14;

            then (x,y) // A by A8, AFF_1: 43;

            hence y in A by A6, A13, AFF_1: 23;

          end;

          then B9 c= A by SUBSET_1: 2;

          hence thesis by A6, A12, XBOOLE_0:def 10;

        end;

         A15:

        now

          K is being_line by A1, AFF_1: 26;

          then

          consider M such that

           A16: a in M and

           A17: K // M by AFF_1: 49;

          

           A18: M is being_line by A17, AFF_1: 36;

          consider A9 such that

           A19: a in A9 and

           A20: A // A9 by A6, AFF_1: 49;

          

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

          assume that

           A22: not A // K and

           A23: A <> K;

          consider p such that

           A24: p in A and

           A25: p in K by A4, A6, A22, AFF_1: 58;

           not A9 // K by A22, A20, AFF_1: 44;

          then

          consider q such that

           A26: q in A9 and

           A27: q in K by A4, A21, AFF_1: 58;

          set C9 = ( Line (q,b));

          

           A28: q in C9 by AFF_1: 15;

          (a,b) // M by A1, A17, AFF_1: 43;

          then b in M by A16, A18, AFF_1: 23;

          then q <> b by A2, A16, A17, A27, AFF_1: 45;

          then C9 is being_line by AFF_1:def 3;

          then

          consider C such that

           A29: p in C and

           A30: C9 // C by AFF_1: 49;

          

           A31: b in C9 by AFF_1: 15;

          

           A32: C is being_line by A30, AFF_1: 36;

          now

            let y such that

             A33: y in C;

             A34:

            now

              

               A35: (q,b) // (p,y) by A28, A31, A29, A30, A33, AFF_1: 39;

              K is being_line by A1, AFF_1: 26;

              then

              consider N such that

               A36: y in N and

               A37: K // N by AFF_1: 49;

              

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

               not N // A by A22, A37, AFF_1: 44;

              then

              consider x such that

               A39: x in N and

               A40: x in A by A6, A38, AFF_1: 58;

              

               A41: (x,y) // K by A36, A37, A39, AFF_1: 40;

              assume

               A42: y <> p;

              

               A43: not x in K

              proof

                assume x in K;

                then y in K by A36, A37, A39, AFF_1: 45;

                then C9 // K by A4, A25, A29, A30, A32, A33, A42, AFF_1: 18;

                hence contradiction by A5, A27, A28, A31, AFF_1: 45;

              end;

              (q,a) // (p,x) by A24, A19, A20, A26, A40, AFF_1: 39;

              then y = (f . x) by A3, A25, A27, A43, A35, A41;

              hence y in B9 by A40, TRANSGEO: 91;

            end;

            now

              assume

               A44: y = p;

              (f . p) = p by A3, A25;

              hence y in B9 by A24, A44, TRANSGEO: 91;

            end;

            hence y in B9 by A34;

          end;

          then

           A45: C c= B9 by SUBSET_1: 2;

          now

            let y;

            assume y in B9;

            then

            consider x such that

             A46: x in A and

             A47: y = (f . x) by TRANSGEO: 91;

            now

              K is being_line by A1, AFF_1: 26;

              then

              consider N such that

               A48: x in N and

               A49: K // N by AFF_1: 49;

              

               A50: not C // N

              proof

                assume C // N;

                then C9 // N by A30, AFF_1: 44;

                then

                 A51: C9 // K by A49, AFF_1: 44;

                q in C9 by AFF_1: 15;

                then C9 = K by A27, A51, AFF_1: 45;

                hence contradiction by A5, AFF_1: 15;

              end;

              N is being_line by A49, AFF_1: 36;

              then

              consider z such that

               A52: z in C and

               A53: z in N by A32, A50, AFF_1: 58;

              

               A54: (x,z) // K by A48, A49, A53, AFF_1: 40;

              assume x <> p;

              then

               A55: not x in K by A4, A6, A23, A24, A25, A46, AFF_1: 18;

              

               A56: (q,a) // (p,x) by A24, A19, A20, A26, A46, AFF_1: 39;

              (q,b) // (p,z) by A28, A31, A29, A30, A52, AFF_1: 39;

              hence y in C by A3, A25, A27, A47, A55, A52, A56, A54;

            end;

            hence y in C by A3, A25, A29, A47;

          end;

          then B9 c= C by SUBSET_1: 2;

          hence thesis by A32, A45, XBOOLE_0:def 10;

        end;

        now

          assume

           A57: A = K;

          now

            let y;

            assume y in B9;

            then ex x st x in A & y = (f . x) by TRANSGEO: 91;

            hence y in A by A3, A57;

          end;

          then

           A58: B9 c= A by SUBSET_1: 2;

          now

            let x such that

             A59: x in A;

            set y = (f . x);

            y in B9 by A59, TRANSGEO: 90;

            hence x in B9 by A3, A57, A59;

          end;

          then A c= B9 by SUBSET_1: 2;

          hence thesis by A6, A58, XBOOLE_0:def 10;

        end;

        hence thesis by A7, A15;

      end;

      hence thesis by TRANSGEO: 96;

    end;

    

     Lm28: ((a,b) // K & not a in K & for x, y holds ((f . x) = y iff (x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K)))) implies f is_Sc K by Lm26, AFF_1: 26, Lm27;

    theorem :: HOMOTHET:8

    

     Th8: (a,b) // K & not a in K & AFP is Moufangian implies ex f st f is_Sc K & (f . a) = b

    proof

      assume that

       A1: (a,b) // K and

       A2: not a in K and

       A3: AFP is Moufangian;

      consider f such that

       A4: for x, y holds ((f . x) = y iff (x in K & x = y or ( not x in K & ex p, p9 st p in K & p9 in K & (p,a) // (p9,x) & (p,b) // (p9,y) & (x,y) // K))) by A1, A2, A3, Lm24;

      

       A5: (f . a) = b by A1, A2, A4, Lm25;

      f is_Sc K by A1, A2, A4, Lm28;

      hence thesis by A5;

    end;

    theorem :: HOMOTHET:9

    AFP is Moufangian iff for a, b, K st (a,b) // K & not a in K holds ex f st f is_Sc K & (f . a) = b by Th6, Th8;