The abstract of the Mizar article:

Elementary Variants of Affine Configurational Theorems

by

Krzysztof Prazmowski, and

Krzysztof Radziszewski

Received November 30, 1990

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