:: Fundamental Types of Metric Affine Spaces
::  by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received April 17, 1991
:: Copyright (c) 1991-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 ANALMETR, SUBSET_1, SYMSP_1, AFF_2, VECTSP_1, TRANSGEO, ANALOAF,
      DIRAF, STRUCT_0, AFF_1, INCSP_1, CONAFFM, CONMETR, RLVECT_1, ARYTM_1,
      ARYTM_3, REAL_1, RELAT_1, CARD_1, MCART_1, SUPINF_2, PARSP_1, EUCLMETR;
 notations SUBSET_1, NUMBERS, STRUCT_0, REAL_1, RLVECT_1, ANALOAF, DIRAF,
      AFF_1, AFF_2, ANALMETR, GEOMTRAP, PAPDESAF, CONMETR, CONAFFM;
 constructors REAL_1, AFF_1, AFF_2, TRANSLAC, GEOMTRAP, CONAFFM, CONMETR;
 registrations ANALMETR, PAPDESAF, REAL_1, ORDINAL1, XREAL_0, STRUCT_0;
 requirements NUMERALS, SUBSET, ARITHM, BOOLE;
 definitions RLVECT_1;
 theorems RLVECT_1, AFF_1, AFF_4, AFPROJ, ANALOAF, ANALMETR, GEOMTRAP,
      PAPDESAF, CONMETR, CONAFFM, AFF_2, RLSUB_2, XCMPLX_1;

begin

definition
  let IT be OrtAfSp;
  attr IT is Euclidean means
  :Def1:
  for a,b,c,d being Element
  of IT st a,b _|_ c,d & b,c _|_ a,d holds b,d _|_ a,c;
end;

definition
  let IT be OrtAfSp;
  attr IT is Pappian means
  :Def2:
  Af(IT) is Pappian;
end;

definition
  let IT be OrtAfSp;
  attr IT is Desarguesian means
  :Def3:
  Af(IT) is Desarguesian;
end;

definition
  let IT be OrtAfSp;
  attr IT is Fanoian means
  :Def4:
  Af(IT) is Fanoian;
end;

definition
  let IT be OrtAfSp;
  attr IT is Moufangian means
  :Def5:
  Af(IT) is Moufangian;
end;

definition
  let IT be OrtAfSp;
  attr IT is translation means
  :Def6:
  Af(IT) is translational;
end;

definition
  let IT be OrtAfSp;
  attr IT is Homogeneous means
  :Def7:
  for o,a,a1,b,b1,c,c1 being Element of IT
st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 &
  not o,c // o,a & not o,a // o,b holds b,c _|_ b1,c1;
end;

reserve MS for OrtAfPl;
reserve MP for OrtAfSp;

theorem Th1:
  for a,b,c being Element of MP st not LIN a,b,c holds a<>b & b<>c & a<>c
proof
  let a,b,c be Element of MP such that
A1: not LIN a,b,c;
  reconsider b9=b,a9=a,c9=c as Element of Af(MP) by ANALMETR:35;
  assume not thesis;
  then LIN a9,b9,c9 by AFF_1:7;
  hence contradiction by A1,ANALMETR:40;
end;

theorem Th2:
  for a,b,c,d being Element of MS, K being Subset of the carrier of
  MS st a,b _|_ K & c,d _|_ K holds a,b // c,d & a,b // d,c
proof
  let a,b,c,d be Element of MS, K be Subset of MS such that
A1: a,b _|_ K and
A2: c,d _|_ K;
  reconsider K9=K as Subset of Af(MS) by ANALMETR:42;
  K is being_line by A1,ANALMETR:44;
  then K9 is being_line by ANALMETR:43;
  then consider p9,q9 being Element of Af(MS) such that
A3: p9 in K9 & q9 in K9 and
A4: p9 <> q9 by AFF_1:19;
  reconsider p=p9,q=q9 as Element of MS by ANALMETR:35;
  a,b _|_ p,q & c,d _|_ p,q by A1,A2,A3,ANALMETR:53;
  hence a,b // c,d by A4,ANALMETR:63;
  hence thesis by ANALMETR:59;
end;

theorem
  for a,b being Element of MS, A,K being Subset of the carrier of MS st
  a<>b & (a,b _|_ K or b,a _|_ K) & a,b _|_ A holds K // A
proof
  let a,b be Element of MS, A,K be Subset of MS such that
A1: a<>b and
A2: a,b _|_ K or b,a _|_ K and
A3: a,b _|_ A;
  a,b _|_ K by A2,ANALMETR:49;
  then consider p,q being Element of MS such that
A4: p<>q & K = Line(p,q) and
A5: a,b _|_ p,q by ANALMETR:def 13;
  consider r,s being Element of MS such that
A6: r<>s & A = Line(r,s) and
A7: a,b _|_ r,s by A3,ANALMETR:def 13;
  p,q // r,s by A1,A5,A7,ANALMETR:63;
  hence thesis by A4,A6,ANALMETR:def 15;
end;

theorem Th4:
  for x,y,z being Element of MP st LIN x,y,z holds LIN x,z,y & LIN
  y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x
proof
  let x,y,z be Element of MP such that
A1: LIN x,y,z;
  reconsider x9=x,y9=y,z9=z as Element of Af(MP) by ANALMETR:35;
A2: LIN x9,y9,z9 by A1,ANALMETR:40;
  then
A3: LIN y9,z9,x9 & LIN z9,x9,y9 by AFF_1:6;
A4: LIN z9,y9,x9 by A2,AFF_1:6;
  LIN x9,z9,y9 & LIN y9,x9,z9 by A2,AFF_1:6;
  hence thesis by A3,A4,ANALMETR:40;
end;

theorem Th5:
  for a,b,c being Element of MS st not LIN a,b,c ex d being Element
  of MS st d,a _|_ b,c & d,b _|_ a,c
proof
  let a,b,c be Element of MS;
  set A=Line(a,c),K=Line(b,c);
  reconsider A9=A,K9=K as Subset of Af(MS) by ANALMETR:42;
  reconsider a9=a,b9=b,c9=c as Element of Af(MS) by ANALMETR:35;
  K9=Line(b9,c9) by ANALMETR:41;
  then
A1: b9 in K9 & c9 in K9 by AFF_1:15;
  assume
A2: not LIN a,b,c;
  then a<>c by Th1;
  then A is being_line by ANALMETR:def 12;
  then consider P being Subset of MS such that
A3: b in P and
A4: A _|_ P by CONMETR:3;
  b<>c by A2,Th1;
  then K is being_line by ANALMETR:def 12;
  then consider Q being Subset of MS such that
A5: a in Q and
A6: K _|_ Q by CONMETR:3;
  reconsider P9=P,Q9=Q as Subset of Af(MS) by ANALMETR:42;
  Q is being_line by A6,ANALMETR:44;
  then
A7: Q9 is being_line by ANALMETR:43;
A8: A9=Line(a9,c9) by ANALMETR:41;
  then
A9: c9 in A9 by AFF_1:15;
A10: not P9 // Q9
  proof
    assume not thesis;
    then P // Q by ANALMETR:46;
    then A _|_ Q by A4,ANALMETR:52;
    then A // K by A6,ANALMETR:65;
    then A9 // K9 by ANALMETR:46;
    then b9 in A9 by A9,A1,AFF_1:45;
    then LIN a9,c9,b9 by A8,AFF_1:def 2;
    then LIN a9,b9,c9 by AFF_1:6;
    hence contradiction by A2,ANALMETR:40;
  end;
  P is being_line by A4,ANALMETR:44;
  then P9 is being_line by ANALMETR:43;
  then consider d9 being Element of Af(MS) such that
A11: d9 in P9 & d9 in Q9 by A7,A10,AFF_1:58;
  reconsider d=d9 as Element of MS by ANALMETR:35;
  take d;
  a9 in A9 by A8,AFF_1:15;
  hence thesis by A3,A4,A5,A6,A9,A1,A11,ANALMETR:56;
end;

theorem Th6:
  for a,b,c,d1,d2 being Element of MS st not LIN a,b,c & d1,a _|_ b
  ,c & d1,b _|_ a,c & d2,a _|_ b,c & d2,b _|_ a,c holds d1=d2
proof
  let a,b,c,d1,d2 be Element of MS such that
A1: not LIN a,b,c and
A2: d1,a _|_ b,c and
A3: d1,b _|_ a,c and
A4: d2,a _|_ b,c and
A5: d2,b _|_ a,c;
  reconsider a9=a,b9=b,c9=c,d19=d1,d29=d2 as Element of Af(MS) by ANALMETR:35;
  assume
A6: d1<>d2;
  b<>c by A1,Th1;
  then d1,a // d2,a by A2,A4,ANALMETR:63;
  then d19,a9 // d29,a9 by ANALMETR:36;
  then a9,d19 // a9, d29 by AFF_1:4;
  then LIN a9,d19,d29 by AFF_1:def 1;
  then
A7: LIN d19,d29,a9 by AFF_1:6;
  a<>c by A1,Th1;
  then d1,b // d2,b by A3,A5,ANALMETR:63;
  then d19,b9 // d29,b9 by ANALMETR:36;
  then b9,d19 // b9,d29 by AFF_1:4;
  then LIN b9,d19,d29 by AFF_1:def 1;
  then
A8: LIN d19,d29,b9 by AFF_1:6;
  set X9=Line(a9,b9);
  reconsider X=X9 as Subset of MS by ANALMETR:42;
A9: b<>a by A1,Th1;
  then
A10: X9 is being_line by AFF_1:def 3;
  then
A11: X is being_line by ANALMETR:43;
A12: a9 in X9 by AFF_1:15;
A13: b9 in X9 by AFF_1:15;
  LIN d19,d29,d29 by AFF_1:7;
  then
A14: d2 in X by A6,A9,A7,A8,A10,A12,A13,AFF_1:8,25;
  LIN d19,d29,d19 by AFF_1:7;
  then
A15: d1 in X by A6,A9,A7,A8,A10,A12,A13,AFF_1:8,25;
  a<>d1 or a<>d2 by A6;
  then
A16: b,c _|_ X by A2,A4,A12,A15,A14,A11,ANALMETR:55;
  b<>d1 or b<>d2 by A6;
  then a,c _|_ X by A3,A5,A13,A15,A14,A11,ANALMETR:55;
  then a,c // b,c by A16,Th2;
  then a9,c9 // b9,c9 by ANALMETR:36;
  then c9,b9 // c9,a9 by AFF_1:4;
  then LIN c9,b9,a9 by AFF_1:def 1;
  then LIN a9,b9,c9 by AFF_1:6;
  hence contradiction by A1,ANALMETR:40;
end;

theorem Th7:
  for a,b,c,d being Element of MS st a,b _|_ c,d & b,c _|_ a,d &
  LIN a,b,c holds (a=c or a=b or b=c)
proof
  let a,b,c,d be Element of MS such that
A1: a,b _|_ c,d and
A2: b,c _|_ a,d and
A3: LIN a,b,c;
  assume
A4: not thesis;
  LIN c,b,a by A3,Th4;
  then c,b // c,a by ANALMETR:def 10;
  then a,c // b,c by ANALMETR:59;
  then
A5: a,c _|_ a,d by A2,A4,ANALMETR:62;
  reconsider a9=a,b9=b,c9=c,d9=d as Element of Af(MS) by ANALMETR:35;
  LIN a9,b9,c9 by A3,ANALMETR:40;
  then consider A9 being Subset of Af(MS) such that
A6: A9 is being_line and
A7: a9 in A9 and
A8: b9 in A9 and
A9: c9 in A9 by AFF_1:21;
  reconsider A=A9 as Subset of MS by ANALMETR:42;
A10: A is being_line by A6,ANALMETR:43;
  then
A11: c,d _|_ A by A1,A4,A7,A8,ANALMETR:55;
  a,b // a,c by A3,ANALMETR:def 10;
  then a,c _|_ c,d by A1,A4,ANALMETR:62;
  then c,d // a,d by A4,A5,ANALMETR:63;
  then d,c // d,a by ANALMETR:59;
  then LIN d,c,a by ANALMETR:def 10;
  then LIN a,c,d by Th4;
  then LIN a9,c9,d9 by ANALMETR:40;
  then d in A by A4,A6,A7,A9,AFF_1:25;
  then
A12: c =d by A9,A11,ANALMETR:51;
  a,d _|_ A by A2,A4,A8,A9,A10,ANALMETR:55;
  hence contradiction by A4,A7,A9,A12,ANALMETR:51;
end;

theorem Th8:
  MS is Euclidean iff MS is satisfying_3H
proof
A1: now
    assume
A2: MS is satisfying_3H;
    now
      let a,b,c,d be Element of MS such that
A3:   a,b _|_ c,d and
A4:   b,c _|_ a,d;
A5:   now
A6:     d,a _|_ c,b & d,c _|_ a,b by A3,A4,ANALMETR:61;
        assume
A7:     not LIN a,b,c;
        then consider d1 being Element of MS such that
A8:     d1,a _|_ b,c and
A9:     d1,b _|_ a,c & d1,c _|_ a,b by A2,CONAFFM:def 3;
A10:    not LIN a,c,b by A7,Th4;
        d1,a _|_ c,b by A8,ANALMETR:61;
        then d,b _|_ a,c by A9,A6,A10,Th6;
        hence b,d _|_ a,c by ANALMETR:61;
      end;
      now
A11:    a=c implies b,d _|_ a,c by ANALMETR:58;
A12:    b=c implies b,d _|_ a,c by A3,ANALMETR:61;
        assume
A13:    LIN a,b,c;
        a=b implies b,d _|_ a,c by A4,ANALMETR:61;
        hence b,d _|_ a,c by A3,A4,A13,A11,A12,Th7;
      end;
      hence b,d _|_ a,c by A5;
    end;
    hence MS is Euclidean by Def1;
  end;
  now
    assume
A14: MS is Euclidean;
    now
      let a,b,c be Element of MS;
      assume not LIN a,b,c;
      then consider d being Element of MS such that
A15:  d,a _|_ b,c & d,b _|_ a,c by Th5;
      take d;
      b,c _|_ a,d & c,a _|_ b,d by A15,ANALMETR:61;
      then c,d _|_ b,a by A14,Def1;
      hence d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b by A15,ANALMETR:61;
    end;
    hence MS is satisfying_3H by CONAFFM:def 3;
  end;
  hence thesis by A1;
end;

theorem Th9:
  MS is Homogeneous iff MS is satisfying_ODES
proof
  MS is satisfying_ODES iff for o,a,a1,b,b1,c,c1 being Element of MS st o,
a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not
  o,c // o,a & not o,a // o,b holds b,c _|_ b1,c1 by CONAFFM:def 4;
  hence thesis by Def7;
end;

Lm1: MS is satisfying_PAP iff Af MS is Pappian
proof
  set AS=Af(MS);
A1: now
    assume
A2: MS is satisfying_PAP;
    now
      let M,N be Subset of AS, o,a,b,c,a9,b9,c9 be Element of
      AS such that
A3:   M is being_line & N is being_line and
A4:   M<>N and
A5:   o in M & o in N and
A6:   o<>a and
A7:   o<>a9 & o<>b and
A8:   o<>b9 & o<>c & o<>c9 & a in M and
A9:   b in M and
A10:  c in M and
A11:  a9 in N and
A12:  b9 in N & c9 in N and
A13:  a,b9 // b,a9 and
A14:  b,c9 // c,b9;
      reconsider M9=M,N9=N as Subset of MS by ANALMETR:42;
      reconsider a1=a,b1=b,c1=c,a19=a9,b19=b9,c19=c9 as Element
      of MS by ANALMETR:35;
A15:  b1,c19 // c1,b19 by A14,ANALMETR:36;
      a1,b19 // b1,a19 by A13,ANALMETR:36;
      then
A16:  b1,a19 // a1,b19 by ANALMETR:59;
A17:  M9 is being_line & N9 is being_line by A3,ANALMETR:43;
      then ( not a19 in M9)& not b1 in N9 by A4,A5,A7,A9,A11,CONMETR:5;
      then c1,a19 // a1,c19 by A2,A5,A6,A8,A9,A10,A11,A12,A17,A16,A15,
CONMETR:def 2;
      then a1,c19 // c1,a19 by ANALMETR:59;
      hence a,c9 // c,a9 by ANALMETR:36;
    end;
    hence Af MS is Pappian by AFF_2:def 2;
  end;
  now
    assume
A18: Af MS is Pappian;
    now
      let o,a1,a2,a3,b1,b2,b3 be Element of MS, M,N be Subset of the carrier
      of MS such that
A19:  M is being_line & N is being_line and
A20:  o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in
      N & b3 in N & ( not b2 in M)& not a3 in N & o<>a1 & o<>a2 and
      o<>a3 and
A21:  o<>b1 and
      o<>b2 and
A22:  o<>b3 and
A23:  a3,b2 // a2,b1 and
A24:  a3,b3 // a1,b1;
      reconsider M9=M,N9=N as Subset of AS by ANALMETR:42;
      reconsider a=a1,b=a2,c = a3,a9=b1,b9=b2,c9=b3 as Element
      of AS by ANALMETR:35;
A25:  c,c9 // a,a9 by A24,ANALMETR:36;
      a2,b1 // a3,b2 by A23,ANALMETR:59;
      then
A26:  b,a9 // c,b9 by ANALMETR:36;
      M9 is being_line & N9 is being_line by A19,ANALMETR:43;
      then b,c9 // a,b9 by A18,A20,A21,A22,A26,A25,AFF_2:def 2;
      then a2,b3 // a1,b2 by ANALMETR:36;
      hence a1,b2 // a2,b3 by ANALMETR:59;
    end;
    hence MS is satisfying_PAP by CONMETR:def 2;
  end;
  hence thesis by A1;
end;

theorem Th10:
  MS is Pappian iff MS is satisfying_PAP
proof
  set AS=Af(MS);
A1: now
    assume MS is satisfying_PAP;
    then AS is Pappian by Lm1;
    hence MS is Pappian by Def2;
  end;
  now
    assume MS is Pappian;
    then AS is Pappian by Def2;
    hence MS is satisfying_PAP by Lm1;
  end;
  hence thesis by A1;
end;

Lm2: MS is satisfying_DES iff Af MS is Desarguesian
proof
  set AS=Af(MS);
A1: now
    assume
A2: MS is satisfying_DES;
    now
      let A,P,C be Subset of AS, o,a,b,c,a9,b9,c9 be Element of
      AS such that
A3:   o in A and
A4:   o in P and
A5:   o in C and
A6:   o<>a and
A7:   o<>b and
A8:   o<>c and
A9:   a in A and
A10:  a9 in A and
A11:  b in P and
A12:  b9 in P and
A13:  c in C and
A14:  c9 in C and
A15:  A is being_line and
A16:  P is being_line and
A17:  C is being_line and
A18:  A<>P and
A19:  A<>C and
A20:  a,b // a9,b9 and
A21:  a,c // a9,c9;
      now
        reconsider o1=o,a1=a,b1=b,c1=c,a19=a9,b19=b9,c19=c9 as Element of MS
        by ANALMETR:35;
        assume that
A22:    o<>a9 and
A23:    a<>a9;
A24:    a1,b1 // a19,b19 & a1,c1 // a19,c19 by A20,A21,ANALMETR:36;
A25:    b<>b9 by A3,A4,A6,A7,A9,A10,A11,A15,A16,A18,A20,A23,AFF_4:9;
        now
          assume LIN b,b9,a;
          then a in P by A11,A12,A16,A25,AFF_1:25;
          hence contradiction by A3,A4,A6,A9,A15,A16,A18,AFF_1:18;
        end;
        then
A26:    not LIN b1,b19,a1 by ANALMETR:40;
        LIN o,a,a9 by A3,A9,A10,A15,AFF_1:21;
        then
A27:    LIN o1,a1,a19 by ANALMETR:40;
        now
          assume LIN a,a9,c;
          then c in A by A9,A10,A15,A23,AFF_1:25;
          hence contradiction by A3,A5,A8,A13,A15,A17,A19,AFF_1:18;
        end;
        then
A28:    not LIN a1,a19,c1 by ANALMETR:40;
        LIN o,b,b9 by A4,A11,A12,A16,AFF_1:21;
        then
A29:    LIN o1,b1,b19 by ANALMETR:40;
        LIN o,c,c9 by A5,A13,A14,A17,AFF_1:21;
        then
A30:    LIN o1,c1,c19 by ANALMETR:40;
        o1<>b19 & o1<>c19 by A3,A4,A5,A6,A7,A8,A9,A10,A11,A13,A15,A16,A17,A18
,A19,A20,A21,A22,AFF_4:8;
        then b1,c1 // b19,c19 by A2,A6,A7,A8,A22,A27,A29,A30,A24,A26,A28,
CONAFFM:def 1;
        hence b,c // b9,c9 by ANALMETR:36;
      end;
      hence
      b,c // b9,c9 by A3,A4,A5,A6,A7,A8,A9,A11,A12,A13,A14,A15,A16,A17,A18,A19
,A20,A21,AFPROJ:50;
    end;
    hence AS is Desarguesian by AFF_2:def 4;
  end;
  now
    assume
A31: AS is Desarguesian;
    now
      let o,a,a1,b,b1,c,c1 be Element of MS such that
A32:  o<>a and
      o<>a1 and
A33:  o<>b and
      o<>b1 and
A34:  o<>c and
      o<>c1 and
A35:  not LIN b,b1,a and
A36:  not LIN a,a1,c and
A37:  LIN o,a,a1 and
A38:  LIN o,b,b1 and
A39:  LIN o,c,c1 and
A40:  a,b // a1,b1 & a,c // a1,c1;
      reconsider o9=o,a9=a,b9=b,c9=c,a19=a1,b19=b1, c19=c1 as Element of AS by
ANALMETR:35;
      LIN o9,a9,a19 by A37,ANALMETR:40;
      then consider A being Subset of AS such that
A41:  A is being_line and
A42:  o9 in A and
A43:  a9 in A and
A44:  a19 in A by AFF_1:21;
      LIN o9,c9,c19 by A39,ANALMETR:40;
      then consider C being Subset of AS such that
A45:  C is being_line & o9 in C and
A46:  c9 in C and
A47:  c19 in C by AFF_1:21;
A48:  A<>C
      proof
        assume A=C;
        then LIN a9,a19,c9 by A41,A43,A44,A46,AFF_1:21;
        hence contradiction by A36,ANALMETR:40;
      end;
      LIN o9,b9,b19 by A38,ANALMETR:40;
      then consider P being Subset of AS such that
A49:  P is being_line and
A50:  o9 in P and
A51:  b9 in P & b19 in P by AFF_1:21;
A52:  A<>P
      proof
        assume A=P;
        then LIN b9,b19,a9 by A43,A49,A51,AFF_1:21;
        hence contradiction by A35,ANALMETR:40;
      end;
      a9,b9 // a19,b19 & a9,c9 // a19,c19 by A40,ANALMETR:36;
      then b9,c9 // b19,c19 by A31,A32,A33,A34,A41,A42,A43,A44,A49,A50,A51,A45
,A46,A47,A52,A48,AFF_2:def 4;
      hence b,c // b1,c1 by ANALMETR:36;
    end;
    hence MS is satisfying_DES by CONAFFM:def 1;
  end;
  hence thesis by A1;
end;

theorem Th11:
  MS is Desarguesian iff MS is satisfying_DES
proof
  set AS=Af(MS);
A1: now
    assume MS is satisfying_DES;
    then AS is Desarguesian by Lm2;
    hence MS is Desarguesian by Def3;
  end;
  now
    assume MS is Desarguesian;
    then AS is Desarguesian by Def3;
    hence MS is satisfying_DES by Lm2;
  end;
  hence thesis by A1;
end;

theorem
  MS is Moufangian iff MS is satisfying_TDES
proof
  set AS=Af(MS);
A1: now
    assume
A2: MS is satisfying_TDES;
    now
      let K be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS
      such that
A3:   K is being_line and
A4:   o in K and
A5:   c in K and
A6:   c9 in K and
A7:   not a in K and
A8:   o<>c and
A9:   a<>b and
A10:  LIN o,a,a9 and
A11:  LIN o,b,b9 and
A12:  a,b // a9,b9 and
A13:  a,c // a9,c9 and
A14:  a,b // K;
      reconsider o1=o,a1=a,b1=b,c1=c,a19=a9,b19=b9,c19=c9 as Element of MS by
ANALMETR:35;
A15:  o1<>b1 & a1,c1 // a19,c19 by A4,A7,A13,A14,AFF_1:35,ANALMETR:36;
A16:  not LIN o,a,c
      proof
        assume not thesis;
        then LIN o,c,a by AFF_1:6;
        hence contradiction by A3,A4,A5,A7,A8,AFF_1:25;
      end;
A17:  not LIN o,a,b
      proof
        set M=Line(a,b);
        assume not thesis;
        then LIN a,b,o by AFF_1:6;
        then
A18:    o in M by AFF_1:def 2;
        a in M & M // K by A9,A14,AFF_1:15,def 5;
        then a in K by A4,A18,AFF_1:45;
        hence contradiction by A3,A4,A5,A16,AFF_1:21;
      end;
      a,b // o,c by A3,A4,A5,A8,A14,AFF_1:27;
      then b,a // o,c by AFF_1:4;
      then
A19:  b1,a1 // o1,c1 by ANALMETR:36;
A20:  LIN o1,a1,a19 & LIN o1,b1,b19 by A10,A11,ANALMETR:40;
      a1,b1 // a19,b19 by A12,ANALMETR:36;
      then
A21:  b1,a1 // b19,a19 by ANALMETR:59;
A22:  LIN o,c,c9 by A3,A4,A5,A6,AFF_1:21;
      then
A23:  LIN o1,c1,c19 by ANALMETR:40;
A24:  now
        assume
A25:    a9<>o;
A26:    now
          assume
A27:      a<>a9;
A28:      not LIN a1,a19,c1
          proof
            assume not thesis;
            then
A29:        LIN a,a9,c by ANALMETR:40;
            LIN a,a9,o & LIN a,a9,a by A10,AFF_1:6,7;
            hence contradiction by A16,A27,A29,AFF_1:8;
          end;
A30:      not LIN a1,a19,b1
          proof
            assume not thesis;
            then
A31:        LIN a,a9,b by ANALMETR:40;
            LIN a,a9,o & LIN a,a9,a by A10,AFF_1:6,7;
            hence contradiction by A17,A27,A31,AFF_1:8;
          end;
          c,a // c9,a9 & not LIN o,c,a by A13,A16,AFF_1:4,6;
          then
A32:      o1<>c19 by A10,A25,AFF_1:55;
          b,a // b9,a9 & not LIN o,b,a by A12,A17,AFF_1:4,6;
          then o1<>b19 by A10,A25,AFF_1:55;
          then b1,c1 // b19,c19 by A2,A4,A7,A8,A20,A23,A21,A19,A15,A25,A32,A28
,A30,CONMETR:def 5;
          hence b,c // b9,c9 by ANALMETR:36;
        end;
        now
A33:      LIN o,c,c by AFF_1:7;
          assume
A34:      a=a9;
          then a,c // a9,c by AFF_1:2;
          then
A35:      c =c9 by A10,A13,A22,A16,A33,AFF_1:56;
A36:      LIN o,b,b by AFF_1:7;
          a,b // a9,b by A34,AFF_1:2;
          then b=b9 by A10,A11,A12,A17,A36,AFF_1:56;
          hence b,c // b9,c9 by A35,AFF_1:2;
        end;
        hence b,c // b9,c9 by A26;
      end;
      now
        assume a9=o;
        then b9=o & c9=o by A11,A12,A13,A22,A16,A17,AFF_1:55;
        hence b,c // b9,c9 by AFF_1:3;
      end;
      hence b,c // b9,c9 by A24;
    end;
    then AS is Moufangian by AFF_2:def 7;
    hence MS is Moufangian by Def5;
  end;
  now
    assume MS is Moufangian;
    then
A37: AS is Moufangian by Def5;
    now
      let o,a,a1,b,b1,c,c1 be Element of MS such that
      o<>a and
      o<>a1 and
A38:  o<>b and
      o<>b1 and
A39:  o<>c and
      o<>c1 and
A40:  not LIN b,b1,a and
A41:  not LIN b,b1,c and
A42:  LIN o,a,a1 and
A43:  LIN o,b,b1 and
A44:  LIN o,c,c1 and
A45:  a,b // a1,b1 and
A46:  a,b // o,c and
A47:  b,c // b1,c1;
      reconsider o9=o,a9=a,a19=a1,b9=b,b19=b1,c9=c,c19=c1 as Element of AS by
ANALMETR:35;
      set K=Line(o9,c9);
A48:  K is being_line by A39,AFF_1:def 3;
      a9,b9 // o9,c9 by A46,ANALMETR:36;
      then a9,b9 // K by A39,AFF_1:def 4;
      then
A49:  b9,a9 // K by AFF_1:34;
      a9,b9 // a19,b19 by A45,ANALMETR:36;
      then
A50:  b9,a9 // b19,a19 by AFF_1:4;
A51:  c9 in K by AFF_1:15;
A52:  LIN o9,a9,a19 & b9,c9 // b19,c19 by A42,A47,ANALMETR:36,40;
A53:  b9<>a9 by A40,Th1;
A54:  o9 in K by AFF_1:15;
A55:  LIN o9,b9,b19 by A43,ANALMETR:40;
A56:  not b9 in K
      proof
        assume
A57:    b9 in K;
        then b19 in K by A38,A48,A54,A55,AFF_1:25;
        then LIN b9,b19,c9 by A48,A51,A57,AFF_1:21;
        hence contradiction by A41,ANALMETR:40;
      end;
      LIN o9,c9,c19 by A44,ANALMETR:40;
      then c19 in K by A39,A48,A54,A51,AFF_1:25;
      then a9,c9 // a19,c19 by A37,A39,A48,A54,A51,A55,A56,A49,A50,A52,A53,
AFF_2:def 7;
      hence a,c // a1,c1 by ANALMETR:36;
    end;
    hence MS is satisfying_TDES by CONMETR:def 5;
  end;
  hence thesis by A1;
end;

Lm3: MS is satisfying_des iff Af MS is translational
proof
  set AS=Af(MS);
A1: now
    assume
A2: MS is satisfying_des;
    now
      let A,P,C be Subset of AS, a,b,c,a9,b9,c9 be Element of AS such that
A3:   A // P and
A4:   A // C and
A5:   a in A and
A6:   a9 in A and
A7:   b in P and
A8:   b9 in P and
A9:   c in C and
A10:  c9 in C and
A11:  A is being_line and
A12:  P is being_line and
A13:  C is being_line and
A14:  A<>P and
A15:  A<>C and
A16:  a,b // a9,b9 and
A17:  a,c // a9,c9;
A18:  not a in C by A4,A5,A15,AFF_1:45;
A19:  now
        reconsider aa=a,a1=a9,bb=b,b1=b9,cc=c,c1=c9 as Element of MS by
ANALMETR:35;
        a,a9 // b,b9 by A3,A5,A6,A7,A8,AFF_1:39;
        then
A20:    aa,a1 // bb,b1 by ANALMETR:36;
        a,a9 // c,c9 by A4,A5,A6,A9,A10,AFF_1:39;
        then
A21:    aa,a1 // cc,c1 by ANALMETR:36;
        assume
A22:    a<>a9;
A23:    not LIN aa,a1,bb
        proof
          assume not thesis;
          then LIN a,a9,b by ANALMETR:40;
          then b in A by A5,A6,A11,A22,AFF_1:25;
          hence contradiction by A3,A7,A14,AFF_1:45;
        end;
A24:    not LIN aa,a1,cc
        proof
          assume not thesis;
          then LIN a,a9,c by ANALMETR:40;
          then c in A by A5,A6,A11,A22,AFF_1:25;
          hence contradiction by A4,A9,A15,AFF_1:45;
        end;
        aa,bb // a1,b1 & aa,cc // a1,c1 by A16,A17,ANALMETR:36;
        then bb,cc // b1,c1 by A2,A23,A24,A20,A21,CONMETR:def 8;
        hence b,c // b9,c9 by ANALMETR:36;
      end;
A25:  not a in P by A3,A5,A14,AFF_1:45;
      now
        assume
A26:    a=a9;
        then LIN a,c,c9 by A17,AFF_1:def 1;
        then LIN c,c9,a by AFF_1:6;
        then
A27:    c = c9 by A9,A10,A13,A18,AFF_1:25;
        LIN a,b,b9 by A16,A26,AFF_1:def 1;
        then LIN b,b9,a by AFF_1:6;
        then b = b9 by A7,A8,A12,A25,AFF_1:25;
        hence b,c // b9,c9 by A27,AFF_1:2;
      end;
      hence b,c // b9,c9 by A19;
    end;
    hence AS is translational by AFF_2:def 11;
  end;
  now
    assume
A28: AS is translational;
    now
      let a,a1,b,b1,c,c1 be Element of MS such that
A29:  ( not LIN a,a1,b)& not LIN a,a1,c and
A30:  a,a1 // b,b1 and
A31:  a,a1 // c,c1 and
A32:  a,b // a1,b1 & a,c // a1,c1;
      reconsider a9=a,a19=a1,b9=b,b19=b1,c9=c,c19=c1 as Element of AS by
ANALMETR:35;
A33:  a9,a19 // b9,b19 by A30,ANALMETR:36;
A34:  a9,b9 // a19,b19 & a9,c9 // a19,c19 by A32,ANALMETR:36;
A35:  a9,a19 // c9,c19 by A31,ANALMETR:36;
      set A=Line(a9,a19);
A36:  not a9,a19 // a9,b9 & not a9,a19 // a9,c9
      proof
        assume not thesis;
        then a,a1 // a,b or a,a1 // a,c by ANALMETR:36;
        hence contradiction by A29,ANALMETR:def 10;
      end;
      then
A37:  a9<>a19 by AFF_1:3;
      then
A38:  A is being_line by AFF_1:def 3;
      then consider C being Subset of AS such that
A39:  c9 in C and
A40:  A // C by AFF_1:49;
A41:  C is being_line by A40,AFF_1:36;
A42:  a9 in A & a19 in A by AFF_1:15;
      then
A43:  A<>C by A36,A38,A39,AFF_1:51;
A44:  a9,a19 // A by A38,A42,AFF_1:23;
      then a9,a19 // C by A40,AFF_1:43;
      then c9,c19 // C by A35,A37,AFF_1:32;
      then
A45:  c19 in C by A39,A41,AFF_1:23;
      consider P being Subset of AS such that
A46:  b9 in P and
A47:  A // P by A38,AFF_1:49;
A48:  P is being_line by A47,AFF_1:36;
      a9,a19 // P by A44,A47,AFF_1:43;
      then b9,b19 // P by A33,A37,AFF_1:32;
      then
A49:  b19 in P by A46,A48,AFF_1:23;
      A<>P by A36,A38,A42,A46,AFF_1:51;
      then
      b9,c9 // b19,c19 by A28,A34,A38,A42,A46,A47,A39,A40,A48,A41,A49,A45,A43,
AFF_2:def 11;
      hence b,c // b1,c1 by ANALMETR:36;
    end;
    hence MS is satisfying_des by CONMETR:def 8;
  end;
  hence thesis by A1;
end;

theorem
  MS is translation iff MS is satisfying_des
proof
  set AS=Af(MS);
A1: now
    assume MS is satisfying_des;
    then AS is translational by Lm3;
    hence MS is translation by Def6;
  end;
  now
    assume MS is translation;
    then AS is translational by Def6;
    hence MS is satisfying_des by Lm3;
  end;
  hence thesis by A1;
end;

theorem Th14:
  MS is Homogeneous implies MS is Desarguesian
proof
  assume MS is Homogeneous;
  then MS is satisfying_ODES by Th9;
  then MS is satisfying_DES by CONAFFM:1;
  hence thesis by Th11;
end;

theorem Th15:
  MS is Euclidean Desarguesian implies MS is Pappian
proof
  assume MS is Euclidean Desarguesian;
  then MS is satisfying_3H & MS is satisfying_DES by Th8,Th11;
  then MS is satisfying_PAP by CONMETR:13,15;
  hence thesis by Th10;
end;

reserve V for RealLinearSpace;
reserve w,y,u,v for VECTOR of V;

theorem Th16:
  for o,c,c1,a,a1,a2 being Element of MS st not LIN o,c,a & o<>c1
  & o,c _|_ o,c1 & o,a _|_ o,a1 & o,a _|_ o,a2 & c,a _|_ c1,a1 & c,a _|_ c1,a2
  holds a1=a2
proof
  let o,c,c1,a,a1,a2 be Element of MS such that
A1: not LIN o,c,a and
A2: o<>c1 & o,c _|_ o,c1 and
A3: o,a _|_ o,a1 & o,a _|_ o,a2 and
A4: c,a _|_ c1,a1 & c,a _|_ c1,a2;
  reconsider o9=o,a19=a1,a29=a2,c19=c1 as Element of Af(MS) by ANALMETR:35;
  assume
A5: a1<>a2;
  o<>a by A1,Th1;
  then o,a1 // o,a2 by A3,ANALMETR:63;
  then o9,a19 // o9,a29 by ANALMETR:36;
  then LIN o9,a19, a29 by AFF_1:def 1;
  then
A6: LIN a19,a29,o9 by AFF_1:6;
  a<>c by A1,Th1;
  then c1,a1 // c1,a2 by A4,ANALMETR:63;
  then c19,a19 // c19,a29 by ANALMETR:36;
  then LIN c19,a19,a29 by AFF_1:def 1;
  then
A7: LIN a19,a29,c19 by AFF_1:6;
  LIN a19,a29,a29 by AFF_1:7;
  then LIN o9,c19,a29 by A5,A6,A7,AFF_1:8;
  then o9,c19 // o9,a29 by AFF_1:def 1;
  then o,c1 // o,a2 by ANALMETR:36;
  then
A8: o,c _|_ o,a2 by A2,ANALMETR:62;
  LIN a19,a29,a19 by AFF_1:7;
  then LIN o9,c19,a19 by A5,A6,A7,AFF_1:8;
  then o9,c19 // o9,a19 by AFF_1:def 1;
  then o,c1 // o,a1 by ANALMETR:36;
  then
A9: o,c _|_ o,a1 by A2,ANALMETR:62;
  o<>a1 or o<>a2 by A5;
  then o,c // o,a by A3,A9,A8,ANALMETR:63;
  hence contradiction by A1,ANALMETR:def 10;
end;

theorem
  for o,c,c1,a being Element of MS st not LIN o,c,a ex a1 being Element
  of MS st o,a _|_ o,a1 & c,a _|_ c1,a1
proof
  let o,c,c1,a be Element of MS such that
A1: not LIN o,c,a;
  set X=Line(c,a),Y=Line(o,a);
  c <>a by A1,Th1;
  then
A2: X is being_line by ANALMETR:def 12;
  then consider X9 being Subset of MS such that
A3: c1 in X9 and
A4: X _|_ X9 by CONMETR:3;
  o<>a by A1,Th1;
  then Y is being_line by ANALMETR:def 12;
  then consider Y9 being Subset of MS such that
A5: o in Y9 and
A6: Y _|_ Y9 by CONMETR:3;
  reconsider X1=X9,Y1=Y9 as Subset of Af(MS) by ANALMETR:42;
  Y9 is being_line by A6,ANALMETR:44;
  then
A7: Y1 is being_line by ANALMETR:43;
  reconsider o9=o,c9=c,a9=a as Element of Af(MS) by ANALMETR:35;
A8: X=Line(c9,a9) by ANALMETR:41;
  then
A9: a in X by AFF_1:15;
  Y=Line(o9,a9) by ANALMETR:41;
  then
A10: o in Y & a in Y by AFF_1:15;
A11: c in X by A8,AFF_1:15;
  not X9 // Y9
  proof
    reconsider X1=X,Y1=Y as Subset of the carrier of Af(MS) by ANALMETR:42;
    assume not thesis;
    then X9 _|_ Y by A6,ANALMETR:52;
    then X // Y by A4,ANALMETR:65;
    then X1 // Y1 by ANALMETR:46;
    then
A12: o in X by A9,A10,AFF_1:45;
    a in X by A8,AFF_1:15;
    hence contradiction by A1,A2,A11,A12,CONMETR:4;
  end;
  then
A13: not X1 // Y1 by ANALMETR:46;
  X9 is being_line by A4,ANALMETR:44;
  then X1 is being_line by ANALMETR:43;
  then consider a19 being Element of Af(MS) such that
A14: a19 in X1 & a19 in Y1 by A7,A13,AFF_1:58;
  reconsider a1=a19 as Element of MS by ANALMETR:35;
  take a1;
  thus thesis by A3,A4,A5,A6,A11,A9,A10,A14,ANALMETR:56;
end;

Lm4: for u,v,y being VECTOR of V holds (u-y)-(v-y)=u-v & (u+y)-(v+y) = u-v
proof
  let u,v,y be VECTOR of V;
  thus (u-y)-(v-y) = (u-y)+(y-v) by RLVECT_1:33
    .= u-v by ANALOAF:1;
  thus (u+y)-(v+y) = (u-(-y))-(v+y) by RLVECT_1:17
    .= (u-(-y))-(v-(-y)) by RLVECT_1:17
    .= (u-(-y))+((-y)-v) by RLVECT_1:33
    .= u-v by ANALOAF:1;
end;

Lm5: Gen w,y implies for a,b,c being Real holds PProJ(w,y,a*w+b*y,(c*b)*w+(-c*
a)*y) = 0 & a*w+b*y,(c*b)*w+(-c*a)*y are_Ort_wrt w,y
proof
  assume
A1: Gen w,y;
  let a,b,c be Real;
A2: pr2(w,y,a*w+b*y)=b & pr2(w,y,(c*b)*w+(-c*a)*y) = -c*a by A1,GEOMTRAP:def 5;
  pr1(w,y,a*w+b*y)=a & pr1(w,y,(c*b)*w+(-c*a)*y) = c*b by A1,GEOMTRAP:def 4;
  hence PProJ (w,y,a*w+b*y,(c*b)*w+(-c*a)*y) = a*(b*c)+b*(-c*a) by A2,
GEOMTRAP:def 6
    .= 0;
  hence thesis by A1,GEOMTRAP:32;
end;

theorem Th18:
  for a,b being Real st Gen w,y & 0.V<>u & 0.V<>v & u,v
  are_Ort_wrt w,y & u=a*w+b*y ex c being Real st c <>0 & v=(c*b)*w+(-c*a)*y
proof
  let a,b be Real such that
A1: Gen w,y and
A2: 0.V<>u and
A3: 0.V<>v and
A4: u,v are_Ort_wrt w,y and
A5: u=a*w+b*y;
  set v9=b*w+(-a)*y;
  v9= (1*b)*w+(-1*a)*y;
  then u,v9 are_Ort_wrt w,y by A1,A5,Lm5;
  then consider a1,b1 being Real such that
A6: a1*v = b1*v9 and
A7: a1<>0 or b1<>0 by A1,A2,A4,ANALMETR:9;
A8: now
    assume
A9: a1=0;
    then 0.V = b1*v9 by A6,RLVECT_1:10;
    then v9=0.V by A7,A9,RLVECT_1:11;
    then b=0 & -a=0 by A1,ANALMETR:def 1;
    then u= 0.V + 0*y by A5,RLVECT_1:10
      .= 0.V + 0.V by RLVECT_1:10
      .= 0.V by RLVECT_1:4;
    hence contradiction by A2;
  end;
  take c =a1"*b1;
A10: now
    assume
A11: b1=0;
    then 0.V = a1*v by A6,RLVECT_1:10;
    hence contradiction by A3,A7,A11,RLVECT_1:11;
  end;
  now
    assume c =0;
    then a1"=0 by A10,XCMPLX_1:6;
    hence contradiction by A8,XCMPLX_1:202;
  end;
  hence c <>0;
  thus v=(a1")*(b1*v9) by A6,A8,ANALOAF:5
    .= c*v9 by RLVECT_1:def 7
    .= c*(b*w) + c*((-a)*y) by RLVECT_1:def 5
    .= (c*b)*w + c*((-a)*y) by RLVECT_1:def 7
    .= (c*b)*w + (c*(-a))*y by RLVECT_1:def 7
    .= (c*b)*w + (-c*a)*y;
end;

theorem Th19:
  Gen w,y & 0.V<>u & 0.V<>v & u,v are_Ort_wrt w,y implies ex c
being Real st for a,b being Real holds a*w+b*y,(c*b)*w+(-c*a)*y are_Ort_wrt w,y
  & (a*w+b*y)-u,((c*b)*w+(-c*a)*y)-v are_Ort_wrt w,y
proof
  assume that
A1: Gen w,y and
A2: 0.V<>u & 0.V<>v and
A3: u,v are_Ort_wrt w,y;
  consider a1,a2 being Real such that
A4: u=a1*w+a2*y by A1,ANALMETR:def 1;
  consider c being Real such that
  c <>0 and
A5: v=(c*a2)*w+(-c*a1)*y by A1,A2,A3,A4,Th18;
  take c;
  let a,b be Real;
  set u9=a*w+b*y,v9=(c*b)*w+(-c*a)*y;
A6: pr1(w,y,u9)=a & pr2(w,y,u9)=b by A1,GEOMTRAP:def 4,def 5;
A7: pr1(w,y,v9) = c*b & pr2(w,y,v9) = -c*a by A1,GEOMTRAP:def 4,def 5;
  pr1(w,y,u)=a1 & pr2(w,y,u)=a2 by A1,A4,GEOMTRAP:def 4,def 5;
  then
A8: PProJ(w,y,u,v9) = a1*(c*b)+a2*(-c*a) by A7,GEOMTRAP:def 6;
  pr1(w,y,v)=c*a2 & pr2(w,y,v)=-c*a1 by A1,A5,GEOMTRAP:def 4,def 5;
  then
A9: PProJ(w,y,u9,v) = (c*a2)*a+(-c*a1)*b by A6,GEOMTRAP:def 6;
  thus a*w+b*y,(c*b)*w+(-c*a)*y are_Ort_wrt w,y by A1,Lm5;
  PProJ(w,y,(a*w+b*y)-u,((c*b)*w+(-c*a)*y)-v) = PProJ(w,y,u9-u,v9)-PProJ(
  w,y,u9-u,v) by A1,GEOMTRAP:30
    .= (PProJ(w,y,u9,v9)-PProJ(w,y,u,v9)) - PProJ(w,y,u9-u,v) by A1,GEOMTRAP:30
    .= (0 - PProJ(w,y,u,v9)) - PProJ(w,y,u9-u,v) by A1,Lm5
    .= (-PProJ(w,y,u,v9)) - (PProJ(w,y,u9,v) - PProJ(w,y,u,v)) by A1,
GEOMTRAP:30
    .= (-PProJ(w,y,u,v9)) - (PProJ(w,y,u9,v) - 0) by A1,A3,GEOMTRAP:32
    .= (-1)*(PProJ(w,y,u,v9) + PProJ(w,y,u9,v));
  hence thesis by A1,A8,A9,GEOMTRAP:32;
end;

Lm6: for w,y being VECTOR of V,a,b,c,d being Real holds (a*w+b*y)-(c*w+d*y) =
(a-c)*w+(b-d)*y
proof
  let w,y be VECTOR of V, a,b,c,d be Real;
  thus (a*w+b*y)-(c*w+d*y) = b*y+(a*w-(c*w+d*y)) by RLVECT_1:def 3
    .= b*y+((a*w-c*w)-d*y) by RLVECT_1:27
    .= b*y+((a-c)*w-d*y) by RLVECT_1:35
    .= ((a-c)*w+b*y)-d*y by RLVECT_1:def 3
    .= (a-c)*w+(b*y-d*y) by RLVECT_1:def 3
    .= (a-c)*w+(b-d)*y by RLVECT_1:35;
end;

Lm7: Gen w,y implies for a,b,c,d being Real st a*w + c*y = b*w + d*y holds a =
b & c = d
proof
  assume
A1: Gen w,y;
  let a,b,c,d be Real;
  assume a*w+c*y=b*w+d*y;
  then 0.V = (a*w+c*y)-(b*w+d*y) by RLVECT_1:15
    .= (a-b)*w+(c-d)*y by Lm6;
  then -b + a =0 & -d + c = 0 by A1,ANALMETR:def 1;
  hence thesis;
end;

theorem Th20:
  Gen w,y & MS = AMSpace(V,w,y) implies MS is satisfying_LIN
proof
  assume that
A1: Gen w,y and
A2: MS=AMSpace(V,w,y);
  now
    let o,a,a1,b,b1,c,c1 be Element of MS such that
A3: o<>a and
    o<>a1 and
A4: o<>b and
    o<>b1 and
A5: o<>c and
A6: o<>c1 and
    a<>b and
A7: o,c _|_ o,c1 and
A8: o,a _|_ o,a1 and
A9: o,b _|_ o,b1 and
A10: not LIN o,c,a and
A11: LIN o,a,b and
    LIN o,a1,b1 and
A12: a,c _|_ a1,c1 and
A13: b,c _|_ b1,c1;
    reconsider q=o,u1=a,u2=b,u3=c,v3=c1 as VECTOR of V by A2,ANALMETR:19;
    consider A1,A2 being Real such that
A14: u1-q=A1*w+A2*y by A1,ANALMETR:def 1;
A15: not LIN o,c,b
    proof
      reconsider o9=o,a9=a,b9=b,c9=c as Element of Af(MS) by ANALMETR:35;
      assume LIN o,c,b;
      then LIN o9,c9,b9 by ANALMETR:40;
      then
A16:  LIN o9,b9,c9 by AFF_1:6;
      LIN o9,a9,b9 by A11,ANALMETR:40;
      then
A17:  LIN o9,b9,a9 by AFF_1:6;
      LIN o9,b9,o9 by AFF_1:7;
      then LIN o9,c9,a9 by A4,A16,A17,AFF_1:8;
      hence contradiction by A10,ANALMETR:40;
    end;
    q,u3,q,v3 are_Ort_wrt w,y by A2,A7,ANALMETR:21;
    then
A18: u3-q,v3-q are_Ort_wrt w,y by ANALMETR:def 3;
    u3-q<>0.V & v3-q<>0.V by A5,A6,RLVECT_1:21;
    then consider r being Real such that
A19: for a9,b9 being Real holds a9*w+b9*y,(r*b9)*w+(-r*a9)*y
are_Ort_wrt w,y & (a9*w+b9*y)-(u3-q),((r*b9)*w+(-r*a9)*y)-(v3-q) are_Ort_wrt w,
    y by A1,A18,Th19;
    o,a // o,b by A11,ANALMETR:def 10;
    then q,u1 '||' q,u2 by A2,GEOMTRAP:4;
    then q,u1 // q,u2 or q,u1 // u2,q by GEOMTRAP:def 1;
    then consider a9,b9 being Real such that
A20: a9*(u1-q)=b9*(u2-q) and
A21: a9<>0 or b9<>0 by ANALMETR:14;
    consider B1,B2 being Real such that
A22: u2-q=B1*w+B2*y by A1,ANALMETR:def 1;
    set s=b9"*a9;
A23: u1-q<>0.V by A3,RLVECT_1:21;
    now
      assume
A24:  b9=0;
      then 0.V = a9*(u1-q) by A20,RLVECT_1:10;
      hence contradiction by A23,A21,A24,RLVECT_1:11;
    end;
    then
A25: u2-q = b9"*(a9*(u1-q)) by A20,ANALOAF:5
      .= s*(u1-q) by RLVECT_1:def 7;
    then B1*w+B2*y = s*(A1*w)+s*(A2*y) by A14,A22,RLVECT_1:def 5
      .= (s*A1)*w + s*(A2*y) by RLVECT_1:def 7
      .= (s*A1)*w+(s*A2)*y by RLVECT_1:def 7;
    then
A26: B1=s*A1 & B2=s*A2 by A1,Lm7;
    set v19=((r*A2)*w+(-r*A1)*y)+q,v29=((r*B2)*w+(-r*B1)*y)+q;
    reconsider a19=v19,b19=v29 as Element of MS by A2,ANALMETR:19;
A27: v29-q = (r*B2)*w+(-r*B1)*y by RLSUB_2:61
      .= (r*B2)*w+(r*B1)*(-y) by RLVECT_1:24
      .= (r*(s*A2))*w - (r*(s*A1))*y by A26,RLVECT_1:25
      .= r*((s*A2)*w) - (r*(s*A1))*y by RLVECT_1:def 7
      .= r*((s*A2)*w) - r*((s*A1)*y) by RLVECT_1:def 7
      .= r*((s*A2)*w - (s*A1)*y) by RLVECT_1:34
      .= r*(s*(A2*w) - (s*A1)*y) by RLVECT_1:def 7
      .= r*(s*(A2*w) - s*(A1*y)) by RLVECT_1:def 7
      .= r*(s*(A2*w - A1*y)) by RLVECT_1:34
      .= (s*r)*(A2*w - A1*y) by RLVECT_1:def 7
      .= s*(r*(A2*w - A1*y)) by RLVECT_1:def 7
      .= s*(r*(A2*w) - r*(A1*y)) by RLVECT_1:34
      .= s*((r*A2)*w - r*(A1*y)) by RLVECT_1:def 7
      .= s*((r*A2)*w + - (r*A1)*y) by RLVECT_1:def 7
      .= s*( (r*A2)*w + (r*A1)*(-y)) by RLVECT_1:25
      .= s*((r*A2)*w + (-r*A1)*y) by RLVECT_1:24
      .= s*(v19-q) by RLSUB_2:61;
A28: v29-q=(r*B2)*w+(-r*B1)*y by RLSUB_2:61;
    then u2-q,v29-q are_Ort_wrt w,y by A19,A22;
    then q,u2,q,v29 are_Ort_wrt w,y by ANALMETR:def 3;
    then
A29: o,b _|_ o,b19 by A2,ANALMETR:21;
    1*(u2-v29) = u2-v29 by RLVECT_1:def 8
      .= s*(u1-q)-s*(v19-q) by A25,A27,Lm4
      .= s*((u1-q)-(v19-q)) by RLVECT_1:34
      .= s*(u1-v19) by Lm4;
    then v19,u1 // v29,u2 or v19,u1 // u2,v29 by ANALMETR:14;
    then v19,u1 '||' v29,u2 by GEOMTRAP:def 1;
    then
A30: a19,a // b19,b by A2,GEOMTRAP:4;
A31: v19-q=(r*A2)*w+(-r*A1)*y by RLSUB_2:61;
    then u1-q,v19-q are_Ort_wrt w,y by A19,A14;
    then q,u1,q,v19 are_Ort_wrt w,y by ANALMETR:def 3;
    then
A32: o,a _|_ o,a19 by A2,ANALMETR:21;
    (u2-q)-(u3-q)=u2-u3 & (v29-q)-(v3-q)=v29-v3 by Lm4;
    then u2-u3,v29-v3 are_Ort_wrt w,y by A19,A22,A28;
    then u3,u2,v3,v29 are_Ort_wrt w,y by ANALMETR:def 3;
    then
A33: c,b _|_ c1,b19 by A2,ANALMETR:21;
    c,b _|_ c1,b1 by A13,ANALMETR:61;
    then
A34: b1=b19 by A6,A7,A9,A15,A29,A33,Th16;
    (u1-q)-(u3-q)=u1-u3 & (v19-q)-(v3-q)=v19-v3 by Lm4;
    then u1-u3,v19-v3 are_Ort_wrt w,y by A19,A14,A31;
    then u3,u1,v3,v19 are_Ort_wrt w,y by ANALMETR:def 3;
    then
A35: c,a _|_ c1,a19 by A2,ANALMETR:21;
    c,a _|_ c1,a1 by A12,ANALMETR:61;
    then a1=a19 by A6,A7,A8,A10,A32,A35,Th16;
    hence a,a1 // b,b1 by A34,A30,ANALMETR:59;
  end;
  hence thesis by CONAFFM:def 5;
end;

theorem Th21:
  for o,a,a1,b,b1,c,c1 being Element of MS st o,b _|_ o,b1 & o,c
_|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & o=
  a1 holds b,c _|_ b1,c1
proof
  let o,a,a1,b,b1,c,c1 be Element of MS such that
A1: o,b _|_ o,b1 and
A2: o,c _|_ o,c1 and
A3: a,b _|_ a1,b1 and
A4: a,c _|_ a1,c1 and
A5: not o,c // o,a and
A6: not o,a // o,b and
A7: o=a1;
A8: o=c1
  proof
    assume o<>c1;
    then a,c // o,c by A2,A4,A7,ANALMETR:63;
    then c,a // c,o by ANALMETR:59;
    then LIN c,a,o by ANALMETR:def 10;
    then LIN o,c,a by Th4;
    hence contradiction by A5,ANALMETR:def 10;
  end;
  o=b1
  proof
    assume o<>b1;
    then a,b // o,b by A1,A3,A7,ANALMETR:63;
    then b,a // b,o by ANALMETR:59;
    then LIN b,a,o by ANALMETR:def 10;
    then LIN o,a,b by Th4;
    hence contradiction by A6,ANALMETR:def 10;
  end;
  hence thesis by A8,ANALMETR:58;
end;

theorem Th22:
  Gen w,y & MS = AMSpace(V,w,y) implies MS is Homogeneous
proof
  assume that
A1: Gen w,y and
A2: MS=AMSpace(V,w,y);
  now
    let o,a,a1,b,b1,c,c1 be Element of MS such that
A3: o,a _|_ o,a1 and
A4: o,b _|_ o,b1 and
A5: o,c _|_ o,c1 and
A6: a,b _|_ a1,b1 and
A7: a,c _|_ a1,c1 and
A8: ( not o,c // o,a)& not o,a // o,b;
    reconsider q=o,u1=a,u2=b,u3=c,v1=a1 as VECTOR of V by A2,ANALMETR:19;
A9: not LIN o,a,b & not LIN o,a,c
    proof
      assume not thesis;
      then o,a // o,b or o,a // o,c by ANALMETR:def 10;
      hence contradiction by A8,ANALMETR:59;
    end;
    then
A10: o<>a by Th1;
    now
      q,u1,q,v1 are_Ort_wrt w,y by A2,A3,ANALMETR:21;
      then
A11:  u1-q,v1-q are_Ort_wrt w,y by ANALMETR:def 3;
A12:  u1-q<>0.V by A10,RLVECT_1:21;
      assume
A13:  o<>a1;
      then v1-q<>0.V by RLVECT_1:21;
      then consider r being Real such that
A14:  for a9,b9 being Real holds a9*w+b9*y,(r*b9)*w+(-r*a9)*y
are_Ort_wrt w,y & (a9*w+b9*y)-(u1-q),((r*b9)*w+(-r*a9)*y)-(v1-q) are_Ort_wrt w,
      y by A1,A11,A12,Th19;
      consider B1,B2 being Real such that
A15:  u2-q=B1*w+B2*y by A1,ANALMETR:def 1;
      consider A1,A2 being Real such that
A16:  u3-q=A1*w+A2*y by A1,ANALMETR:def 1;
      set v39=((r*A2)*w+(-r*A1)*y)+q,v29=((r*B2)*w+(-r*B1)*y)+q;
      reconsider c19=v39,b19=v29 as Element of MS by A2,ANALMETR:19;
A17:  v29-q=(r*B2)*w+(-r*B1)*y by RLSUB_2:61;
      (u2-q)-(u1-q)=u2-u1 & (v29-q)-(v1-q)=v29-v1 by Lm4;
      then u2-u1,v29-v1 are_Ort_wrt w,y by A14,A15,A17;
      then u1,u2,v1,v29 are_Ort_wrt w,y by ANALMETR:def 3;
      then
A18:  a,b _|_ a1,b19 by A2,ANALMETR:21;
      u2-q,v29-q are_Ort_wrt w,y by A14,A15,A17;
      then q,u2,q,v29 are_Ort_wrt w,y by ANALMETR:def 3;
      then o,b _|_ o,b19 by A2,ANALMETR:21;
      then
A19:  b1=b19 by A3,A4,A6,A9,A13,A18,Th16;
A20:  v39-q=(r*A2)*w+(-r*A1)*y by RLSUB_2:61;
      u3-u2 = (A1*w+A2*y)-(B1*w+B2*y) by A16,A15,Lm4
        .= (A1-B1)*w+(A2-B2)*y by Lm6;
      then
A21:  pr1(w,y,u3-u2)=A1-B1 & pr2(w,y,u3-u2)=A2-B2 by A1,GEOMTRAP:def 4,def 5;
      v39-v29 = ((r*A2)*w+(r*(-A1))*y) - ((r*B2)*w+(-r*B1)*y) by Lm4
        .= (r*A2-r*B2)*w + (r*(-A1)-r*(-B1))*y by Lm6
        .= (r*(A2-B2))*w + (r*(B1 -A1))*y;
      then pr1(w,y,v39-v29)=r*(A2-B2) & pr2(w,y,v39-v29)=r*(B1-A1) by A1,
GEOMTRAP:def 4,def 5;
      then
      PProJ (w,y,u3-u2,v39-v29) = (A1-B1)*(r*(A2-B2)) + (A2-B2)*(r*(B1-A1
      )) by A21,GEOMTRAP:def 6
        .=0;
      then u3-u2,v39-v29 are_Ort_wrt w,y by A1,GEOMTRAP:32;
      then
A22:  u2,u3,v29,v39 are_Ort_wrt w,y by ANALMETR:def 3;
      (u3-q)-(u1-q)=u3-u1 & (v39-q)-(v1-q)=v39-v1 by Lm4;
      then u3-u1,v39-v1 are_Ort_wrt w,y by A14,A16,A20;
      then u1,u3,v1,v39 are_Ort_wrt w,y by ANALMETR:def 3;
      then
A23:  a,c _|_ a1,c19 by A2,ANALMETR:21;
      u3-q,v39-q are_Ort_wrt w,y by A14,A16,A20;
      then q,u3,q,v39 are_Ort_wrt w,y by ANALMETR:def 3;
      then o,c _|_ o,c19 by A2,ANALMETR:21;
      then c1=c19 by A3,A5,A7,A9,A13,A23,Th16;
      hence b,c _|_ b1,c1 by A2,A19,A22,ANALMETR:21;
    end;
    hence b,c _|_ b1,c1 by A4,A5,A6,A7,A8,Th21;
  end;
  hence thesis by Def7;
end;

registration
  cluster Euclidean Pappian Desarguesian Homogeneous translation Fanoian
    Moufangian for OrtAfPl;
  existence
  proof
    consider V such that
A1: ex w,y st Gen w,y by ANALMETR:3;
    consider w,y such that
A2: Gen w,y by A1;
    reconsider MS=AMSpace(V,w,y) as OrtAfPl by A2,ANALMETR:34;
A3: MS is satisfying_3H by A2,Th20,CONAFFM:6;
    for a,b being Real st a*w + b*y = 0.V holds a=0 & b=0 by A2,ANALMETR:def 1;
    then reconsider OAS=OASpace(V) as OAffinSpace by ANALOAF:26;
    take MS;
A4: Af(MS)=Lambda(OAS) by ANALMETR:20;
    then
A5: Af(MS) is Moufangian & Af(MS) is translational by PAPDESAF:16,17;
    Af(MS) is Pappian & Af(MS) is Desarguesian by A4,PAPDESAF:13,14;
    hence thesis by A2,A3,A4,A5,Def2,Def3,Def4,Def5,Def6,Th8,Th22;
  end;
end;

registration
  cluster Euclidean Pappian Desarguesian Homogeneous translation Fanoian
    Moufangian for OrtAfSp;
  existence
  proof

set MS = the Euclidean Pappian Desarguesian Homogeneous translation Fanoian
Moufangian OrtAfPl;
    MS is Euclidean Pappian Desarguesian Homogeneous translation Fanoian
    Moufangian;
    hence thesis;
  end;
end;

theorem
  Gen w,y & MS=AMSpace(V,w,y) implies MS is Euclidean Pappian
  Desarguesian Homogeneous translation Fanoian Moufangian OrtAfPl
proof
  assume that
A1: Gen w,y and
A2: MS=AMSpace(V,w,y);
  reconsider MS9=AMSpace(V,w,y) as OrtAfPl by A2;
A3: MS9 is satisfying_3H by A1,Th20,CONAFFM:6;
  for a,b being Real st a*w + b*y = 0.V holds a=0 & b=0 by A1,ANALMETR:def 1;
  then reconsider OAS=OASpace(V) as OAffinSpace by ANALOAF:26;
A4: Af(MS9)=Lambda(OAS) by ANALMETR:20;
  then
A5: Af(MS9) is Moufangian & Af(MS9) is translational by PAPDESAF:16,17;
  Af(MS9) is Pappian & Af(MS9) is Desarguesian by A4,PAPDESAF:13,14;
  hence thesis by A1,A2,A3,A4,A5,Def2,Def3,Def4,Def5,Def6,Th8,Th22;
end;

registration
  let MS be Pappian OrtAfPl;
  cluster Af(MS) -> Pappian;
  correctness by Def2;
end;

registration
  let MS be Desarguesian OrtAfPl;
  cluster Af(MS) -> Desarguesian;
  correctness by Def3;
end;

registration
  let MS be Moufangian OrtAfPl;
  cluster Af(MS) -> Moufangian;
  correctness by Def5;
end;

registration
  let MS be translation OrtAfPl;
  cluster Af(MS) -> translational;
  correctness by Def6;
end;

registration
  let MS be Fanoian OrtAfPl;
  cluster Af(MS) -> Fanoian;
  correctness by Def4;
end;

registration
  let MS be Homogeneous OrtAfPl;
  cluster Af(MS) -> Desarguesian;
  correctness
  proof
    MS is Desarguesian by Th14;
    hence thesis;
  end;
end;

registration
  let MS be Euclidean Desarguesian OrtAfPl;
  cluster Af(MS) -> Pappian;
  correctness
  proof
    MS is Pappian by Th15;
    hence thesis;
  end;
end;

registration
  let MS be Pappian OrtAfSp;
  cluster Af(MS) -> Pappian;
  correctness by Def2;
end;

registration
  let MS be Desarguesian OrtAfSp;
  cluster Af(MS) -> Desarguesian;
  correctness by Def3;
end;

registration
  let MS be Moufangian OrtAfSp;
  cluster Af(MS) -> Moufangian;
  correctness by Def5;
end;

registration
  let MS be translation OrtAfSp;
  cluster Af(MS) -> translational;
  correctness by Def6;
end;

registration
  let MS be Fanoian OrtAfSp;
  cluster Af(MS) -> Fanoian;
  correctness by Def4;
end;