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

### Classical Configurations in Affine Planes

by
Henryk Oryszczyszyn, and
Krzysztof Prazmowski

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