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

Elementary Variants of Affine Configurational Theorems

by
Krzysztof Prazmowski, and

MML identifier: PARDEPAP
[ Mizar article, MML identifier index ]

```environ

vocabulary DIRAF, AFF_2, ANALOAF, AFF_1, INCSP_1, VECTSP_1;
notation SUBSET_1, STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2, PAPDESAF;
constructors TRANSLAC, AFF_1, AFF_2, XBOOLE_0;
clusters PAPDESAF, ZFMISC_1, XBOOLE_0;

begin

reserve SAS for AffinPlane;

theorem :: PARDEPAP:1
SAS satisfies_PAP implies
(for a1,a2,a3,b1,b2,b3 being Element of SAS holds
( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2
implies a3,b1 // a1,b3 ));

theorem :: PARDEPAP:2
SAS satisfies_DES implies
(for o,a,a',b,b',c,c' being Element of SAS holds
( not o,a // o,b & not o,a // o,c & o,a // o,a' & o,b // o,b' &
o,c // o,c' & a,b // a',b' & a,c // a',c' implies b,c // b',c' ));

theorem :: PARDEPAP:3
SAS satisfies_des implies
(for a,a',b,b',c,c' being Element of SAS holds
( not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,a' // c,c' &
a,b // a',b' & a,c // a',c' implies b,c // b',c' ));

canceled;

theorem :: PARDEPAP:5
ex SAS st
(for o,a,a',b,b',c,c' being Element of SAS holds
( not o,a // o,b & not o,a // o,c & o,a // o,a' & o,b // o,b' &
o,c // o,c' & a,b // a',b' & a,c // a',c' implies b,c // b',c' )) &
(for a,a',b,b',c,c' being Element of SAS holds
( not a,a' // a,b & not a,a' // a,c & a,a' // b,b' & a,a' // c,c' &
a,b // a',b' & a,c // a',c' implies b,c // b',c' )) &
(for a1,a2,a3,b1,b2,b3 being Element of SAS holds
( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2
implies a3,b1 // a1,b3 )) &
(for a,b,c,d being Element of SAS holds
( not a,b // a,c & a,b // c,d & a,c // b,d implies not a,d // b,c ));

theorem :: PARDEPAP:6
for o,a being Element of SAS holds
(ex p being Element of SAS st
(for b,c being Element of SAS holds (o,a // o,p &
ex d being Element of SAS st
( o,p // o,b implies o,c // o,d & p,c // b,d ))));
```