Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Affine Localizations of Desargues Axiom

by
Eugeniusz Kusak,
Henryk Oryszczyszyn, and
Krzysztof Prazmowski

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;
```