:: Homotheties and Shears in Affine Planes
::  by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received September 21, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies DIRAF, SUBSET_1, FUNCT_2, STRUCT_0, AFF_2, ANALOAF, INCSP_1,
      AFF_1, TRANSGEO, FUNCT_1, RELAT_1, TARSKI, HOMOTHET;
 notations TARSKI, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, ANALOAF, DIRAF,
      AFF_1, AFF_2, TRANSGEO;
 constructors PARTFUN1, AFF_1, AFF_2, TRANSGEO, RELSET_1;
 registrations STRUCT_0;
 requirements SUBSET, BOOLE;
 theorems TRANSGEO, AFF_1, AFF_2, TRANSLAC, SUBSET_1, DIRAF, FUNCT_1, XBOOLE_0;
 schemes TRANSGEO;

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,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 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 Th2:
  (for o,a,b st o<>a & o<>b & LIN o,a,b 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 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:64;
      then
A14:  LIN o,q,s by AFF_1:def 1;
      set r=f.p;
      o,p // o,r by A11,A12,TRANSGEO:64;
      then
A15:  LIN o,p,r by AFF_1:def 1;
      a,q // a9,s by A11,A13,TRANSGEO:64;
      then
A16:  s=q9 by A2,A4,A6,A8,A14,AFF_1:56;
      a,p // a9,r by A11,A13,TRANSGEO:64;
      then r=p9 by A2,A3,A5,A7,A15,AFF_1:56;
      hence p,q // p9,q9 by A11,A16,TRANSGEO:64;
    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,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,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 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 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 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 ex x st P[x,y] by A2,A3,A4,Lm9;
A6: for x 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:64;
  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 Th3:
  AFP is Desarguesian implies for o,a,b st o<>a & o<>b & LIN o,a,b
  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
  AFP is Desarguesian iff for o,a,b st o<>a & o<>b & LIN o,a,b ex f st f
  is dilatation & f.o=o & f.a=b by Th2,Th3;

definition
  let AFP,f,K;
  pred f is_Sc K means
  :Def1:
  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 Th5:
  f is_Sc K & f.p=p & not p in K implies f=id the carrier of AFP
proof
  assume that
A1: f is_Sc K and
A2: f.p=p and
A3: not p in K;
A4: K is being_line by A1,Def1;
A5: for x st x in K holds f.x=x by A1,Def1;
  f is collineation by A1,Def1;
  hence thesis by A2,A3,A4,A5,TRANSGEO:93;
end;

theorem Th6:
  (for a,b,K st a,b // K & not a in K 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 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,Def1;
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,Def1;
        then
A18:    LIN o,b,x by A6,A13,A14,TRANSGEO:84;
        a9,x // K by A12,Def1;
        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,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,Def1;
    f.c = c by A3,A12,Def1;
    hence b,c // b9,c9 by A11,A13,A14,A21,A16,TRANSGEO:83;
  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))
proof
  assume that
A1: a,b // K and
A2: not a in K and
A3: 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);
  thus thesis by A1,A2,A3,AFF_1:34,35;
end;

Lm19: a,b // K & not a in K implies for x 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,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 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 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,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,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 ex x st P[x,y] by A1,A2,Lm20;
A6: for x 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,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,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:87;
      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:87;
        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:87;
        end;
        now
          assume
A44:      y=p;
          f.p=p by A3,A25;
          hence y in B9 by A24,A44,TRANSGEO:87;
        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:87;
        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:87;
        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:86;
        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:92;
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
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: for x holds x,f.x // K by A1,A3,Lm26;
A5: for x st x in K holds f.x=x by A3;
A6: K is being_line by A1,AFF_1:26;
  f is collineation by A1,A2,A3,Lm27;
  hence thesis by A6,A5,A4,Def1;
end;

theorem 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
  AFP is Moufangian iff for a,b,K st a,b // K & not a in K ex f st f
  is_Sc K & f.a=b by Th6,Th8;