:: Elementary Variants of Affine Configurational Theorems :: by Krzysztof Pra\.zmowski and Krzysztof Radziszewski :: :: Received November 30, 1990 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies DIRAF, AFF_2, SUBSET_1, ANALOAF, AFF_1, INCSP_1, VECTSP_1; notations STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2, PAPDESAF; constructors AFF_1, AFF_2, TRANSLAC; registrations STRUCT_0, PAPDESAF; begin reserve SAS for AffinPlane; theorem :: PARDEPAP:1 SAS is Pappian 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 is Desarguesian implies for o,a,a9,b,b9,c,c9 being Element of SAS holds ( not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 ); theorem :: PARDEPAP:3 SAS is translational implies for a,a9,b,b9,c,c9 being Element of SAS holds ( not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a ,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 ); theorem :: PARDEPAP:4 ex SAS st (for o,a,a9,b,b9,c,c9 being Element of SAS holds ( not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9, b9 & a,c // a9,c9 implies b,c // b9,c9 )) & (for a,a9,b,b9,c,c9 being Element of SAS holds ( not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )) & (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:5 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 ));