The abstract of the Mizar article:

Classical Configurations in Affine Planes

by

Henryk Oryszczyszyn, and

Krzysztof Prazmowski

Received April 13, 1990

MML identifier: AFF_2

[ Mizar article, MML identifier index ]

environ

 vocabulary DIRAF, AFF_1, ANALOAF, INCSP_1, AFF_2;
 notation STRUCT_0, ANALOAF, DIRAF, AFF_1;
 constructors AFF_1, XBOOLE_0;
 clusters ZFMISC_1, XBOOLE_0;


begin

reserve AP for AffinPlane;
reserve a,a',b,b',c,c',x,y,o,p,q,r,s
                     for Element of AP;
reserve A,C,C',D,K,M,N,P,T
             for Subset of AP;

definition let AP;
  attr AP is satisfying_PPAP means
:: AFF_2:def 1
   for M,N,a,b,c,a',b',c' st M is_line & N is_line & a in M &
   b in M & c in M & a' in N & b' in N & c' in N &
   a,b' // b,a' & b,c' // c,b' holds a,c' // c,a';
  synonym AP satisfies_PPAP;
end;

definition let AP be AffinSpace;
  attr AP is Pappian means
:: AFF_2:def 2

   for M,N being Subset of AP,
    o,a,b,c,a',b',c' being Element of AP
     st M is_line & N is_line & M<>N &
   o in M & o in N & o<>a & o<>a' & o<>b & o<>b' & o<>c & o<>c' & a in M &
   b in M & c in M & a' in N & b' in N & c' in N &
   a,b' // b,a' & b,c' // c,b' holds a,c' // c,a';
  synonym AP satisfies_PAP;
end;

definition let AP;
  attr AP is satisfying_PAP_1 means
:: AFF_2:def 3
   for M,N,o,a,b,c,a',b',c' st M is_line & N is_line & M<>N &
   o in M & o in N & o<>a & o<>a' & o<>b & o<>b' & o<>c & o<>c' &
   a in M & b in M & c in M & b' in N & c' in N &
   a,b' // b,a' & b,c' // c,b' & a,c' // c,a' & b<>c holds a' in N;
  synonym AP satisfies_PAP_1;
end;

definition let AP be AffinSpace;
 attr AP is Desarguesian means
:: AFF_2:def 4
   for A,P,C being Subset of AP,
     o,a,b,c,a',b',c'  being Element of AP
    st o in A & o in P & o in C &
   o<>a & o<>b & o<>c & a in A & a' in A & b in P & b' in P &
   c in C & c' in C & A is_line & P is_line & C is_line &
   A<>P & A<>C & a,b // a',b' & a,c // a',c' holds b,c // b',c';
  synonym AP satisfies_DES;
end;

definition let AP;
 attr AP is satisfying_DES_1 means
:: AFF_2:def 5
   for A,P,C,o,a,b,c,a',b',c' st o in A & o in P &
   o<>a & o<>b & o<>c & a in A & a' in A & b in P & b' in P &
   c in C & c' in C & A is_line & P is_line & C is_line &
   A<>P & A<>C & a,b // a',b' & a,c // a',c' & b,c // b',c' &
   not LIN a,b,c & c <>c' holds o in C;
  synonym AP satisfies_DES_1;
end;

definition let AP;
 attr AP is satisfying_DES_2 means
:: AFF_2:def 6
     for A,P,C,o,a,b,c,a',b',c' st o in A & o in P & o in C &
     o<>a & o<>b & o<>c & a in A & a' in A & b in P & b' in P & c in C &
     A is_line & P is_line & C is_line & A<>P & A<>C &
     a,b // a',b' & a,c // a',c' & b,c // b',c' holds c' in C;
  synonym AP satisfies_DES_2;
end;

definition let AP be AffinSpace;
 attr AP is Moufangian means
:: AFF_2:def 7
   for K being Subset of AP,
      o,a,b,c,a',b',c'  being Element of AP
     st K is_line & o in K & c in K & c' in K &
    not a in K & o<>c & a<>b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' &
    a,c // a',c' & a,b // K holds b,c // b',c';
  synonym AP satisfies_TDES;
end;

definition let AP;
 attr AP is satisfying_TDES_1 means
:: AFF_2:def 8
   for K,o,a,b,c,a',b',c' st K is_line & o in K & c in K & c' in K &
   not a in K & o<>c & a<>b & LIN o,a,a' & a,b // a',b' & b,c // b',c' &
   a,c // a',c' & a,b // K holds LIN o,b,b';
  synonym AP satisfies_TDES_1;
end;

definition let AP;
 attr AP is satisfying_TDES_2 means
:: AFF_2:def 9
  for K,o,a,b,c,a',b',c' st K is_line & o in K & c in K & c' in K &
  not a in K & o<>c & a<>b & LIN o,a,a' & LIN o,b,b' & b,c // b',c' &
  a,c // a',c' & a,b // K holds a,b // a',b';
  synonym AP satisfies_TDES_2;
end;

definition let AP;
 attr AP is satisfying_TDES_3 means
:: AFF_2:def 10
   for K,o,a,b,c,a',b',c' st K is_line & o in K & c in K &
   not a in K & o<>c & a<>b & LIN o,a,a' & LIN o,b,b' & a,b // a',b' &
    a,c // a',c' & b,c // b',c' & a,b // K holds c' in K;
  synonym AP satisfies_TDES_3;
end;

definition let AP be AffinSpace;
 attr AP is translational means
:: AFF_2:def 11
   for A,P,C being Subset of AP,
     a,b,c,a',b',c'  being Element of AP
    st A // P & A // C & a in A & a' in A &
    b in P & b' in P & c in C & c' in C & A is_line & P is_line &
    C is_line & A<>P & A<>C & a,b // a',b' & a,c // a',c'
                                                holds b,c // b',c';
  synonym AP satisfies_des;
end;

definition let AP;
 attr AP is satisfying_des_1 means
:: AFF_2:def 12
   for A,P,C,a,b,c,a',b',c' st A // P & a in A & a' in A & b in P &
   b' in P & c in C & c' in C & A is_line & P is_line & C is_line &
   A<>P & A<>C & a,b // a',b' & a,c // a',c' & b,c // b',c' &
   not LIN a,b,c & c <>c' holds A // C;
  synonym AP satisfies_des_1;
end;

definition let AP be AffinSpace;
 attr AP is satisfying_pap means
:: AFF_2:def 13
   for M,N being Subset of AP,
     a,b,c,a',b',c'  being Element of AP
    st M is_line & N is_line &
   a in M & b in M & c in M & M // N & M<>N & a' in N & b' in N & c' in N &
    a,b' // b,a' & b,c' // c,b' holds a,c' // c,a';
  synonym AP satisfies_pap;
end;

definition let AP;
 attr AP is satisfying_pap_1 means
:: AFF_2:def 14
  for M,N,a,b,c,a',b',c' st M is_line & N is_line &
  a in M & b in M & c in M & M // N & M<>N & a' in N & b' in N & a,b' // b,a' &
     b,c' // c,b' & a,c' // c,a' & a'<>b' holds c' in N;
  synonym AP satisfies_pap_1;
end;

canceled 14;

theorem :: AFF_2:15
   AP satisfies_PAP iff AP satisfies_PAP_1;

theorem :: AFF_2:16
   AP satisfies_DES iff AP satisfies_DES_1;

theorem :: AFF_2:17
 AP satisfies_TDES implies AP satisfies_TDES_1;

theorem :: AFF_2:18
   AP satisfies_TDES_1 implies AP satisfies_TDES_2;

theorem :: AFF_2:19
   AP satisfies_TDES_2 implies AP satisfies_TDES_3;

theorem :: AFF_2:20
   AP satisfies_TDES_3 implies AP satisfies_TDES;

theorem :: AFF_2:21
 AP satisfies_des iff AP satisfies_des_1;

theorem :: AFF_2:22
   AP satisfies_pap iff AP satisfies_pap_1;

theorem :: AFF_2:23
 AP satisfies_PAP implies AP satisfies_pap;

theorem :: AFF_2:24
 AP satisfies_PPAP iff AP satisfies_PAP & AP satisfies_pap;

theorem :: AFF_2:25
   AP satisfies_PAP implies AP satisfies_DES;

theorem :: AFF_2:26
   AP satisfies_DES implies AP satisfies_TDES;

theorem :: AFF_2:27
 AP satisfies_TDES_1 implies AP satisfies_des_1;

theorem :: AFF_2:28
   AP satisfies_TDES implies AP satisfies_des;

theorem :: AFF_2:29
   AP satisfies_des implies AP satisfies_pap;