The abstract of the Mizar article:

Affine Localizations of Desargues Axiom

by

Eugeniusz Kusak,

Henryk Oryszczyszyn, and

Krzysztof Prazmowski

Received April 26, 1990

MML identifier: AFF_3

[ Mizar article, MML identifier index ]

environ

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


begin

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


definition let AP;
 attr AP is satisfying_DES1 means
:: AFF_3:def 1
     for A,P,C,o,a,a',b,b',c,c',p,q st
        A is_line & P is_line & C is_line & P<>A & P<>C & A<>C &
        o in A & a in A & a' in A & o in P & b in P & b' in P &
        o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
        not LIN b,a,c & not LIN b',a',c' & a<>a' &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // a',c' holds a,c // p,q;
  synonym AP satisfies_DES1;
end;

definition let AP;
 attr AP is satisfying_DES1_1 means
:: AFF_3:def 2
     for A,P,C,o,a,a',b,b',c,c',p,q st
        A is_line & P is_line & C is_line & P<>A & P<>C & A<>C &
        o in A & a in A & a' in A & o in P & b in P & b' in P &
        o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
        c <>q & not LIN b,a,c & not LIN b',a',c' &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // p,q holds a,c // a',c';
  synonym AP satisfies_DES1_1;
end;

definition let AP;
 attr AP is satisfying_DES1_2 means
:: AFF_3:def 3
     for A,P,C,o,a,a',b,b',c,c',p,q st
       A is_line & P is_line & C is_line & P<>A & P<>C & A<>C &
        o in A & a in A & a' in A & o in P & b in P & b' in P &
        c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
        not LIN b,a,c & not LIN b',a',c' & c <>c' &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // a',c' & a,c // p,q holds o in C;
  synonym AP satisfies_DES1_2;
end;

definition let AP;
 attr AP is satisfying_DES1_3 means
:: AFF_3:def 4
     for A,P,C,o,a,a',b,b',c,c',p,q st
        A is_line & P is_line & C is_line & P<>A & P<>C & A<>C &
        o in A & a in A & a' in A & b in P & b' in P &
        o in C & c in C & c' in C & o<>a & o<>b & o<>c & p<>q &
        not LIN b,a,c & not LIN b',a',c' & b<>b' & a<>a' &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // a',c' & a,c // p,q holds o in P;
  synonym AP satisfies_DES1_3;
end;

definition let AP;
 attr AP is satisfying_DES2 means
:: AFF_3:def 5
     for A,P,C,a,a',b,b',c,c',p,q st
        A is_line & P is_line & C is_line & A<>P & A<>C & P<>C &
        a in A & a' in A & b in P & b' in P & c in C & c' in C &
        A // P & A // C & not LIN b,a,c & not LIN b',a',c' & p<>q &
        a<>a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // a',c' holds a,c // p,q;
  synonym AP satisfies_DES2;
end;

definition let AP;
 attr AP is satisfying_DES2_1 means
:: AFF_3:def 6
     for A,P,C,a,a',b,b',c,c',p,q st
        A is_line & P is_line & C is_line & A<>P & A<>C & P<>C &
        a in A & a' in A & b in P & b' in P & c in C & c' in C &
        A // P & A // C & not LIN b,a,c & not LIN b',a',c' & p<>q &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // p,q holds a,c // a',c';
  synonym AP satisfies_DES2_1;
end;

definition let AP;
 attr AP is satisfying_DES2_2 means
:: AFF_3:def 7
     for A,P,C,a,a',b,b',c,c',p,q st
        A is_line & P is_line & C is_line & A<>P & A<>C & P<>C &
        a in A & a' in A & b in P & b' in P & c in C & c' in C &
        A // C & not LIN b,a,c & not LIN b',a',c' & p<>q & a<>a' &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // a',c' & a,c // p,q holds A // P;
  synonym AP satisfies_DES2_2;
end;

definition let AP;
 attr AP is satisfying_DES2_3 means
:: AFF_3:def 8
     for A,P,C,a,a',b,b',c,c',p,q st
        A is_line & P is_line & C is_line & A<>P & A<>C & P<>C &
        a in A & a' in A & b in P & b' in P & c in C & c' in C &
        A // P & not LIN b,a,c & not LIN b',a',c' & p<>q & c <>c' &
        LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q &
        a,c // a',c' & a,c // p,q holds A // C;
  synonym AP satisfies_DES2_3;
end;

canceled 8;

theorem :: AFF_3:9
   AP satisfies_DES1 implies AP satisfies_DES1_1;

theorem :: AFF_3:10
   AP satisfies_DES1_1 implies AP satisfies_DES1;

theorem :: AFF_3:11
   AP satisfies_DES implies AP satisfies_DES1;

theorem :: AFF_3:12
   AP satisfies_DES implies AP satisfies_DES1_2;

theorem :: AFF_3:13
   AP satisfies_DES1_2 implies AP satisfies_DES1_3;

theorem :: AFF_3:14
   AP satisfies_DES1_2 implies AP satisfies_DES;

theorem :: AFF_3:15
   AP satisfies_DES2_1 implies AP satisfies_DES2;

theorem :: AFF_3:16
   AP satisfies_DES2_1 iff AP satisfies_DES2_3;

theorem :: AFF_3:17
   AP satisfies_DES2 iff AP satisfies_DES2_2;

theorem :: AFF_3:18
   AP satisfies_DES1_3 implies AP satisfies_DES2_1;