:: Elementary Variants of Affine Configurational Theorems
::  by Krzysztof Pra\.zmowski and Krzysztof Radziszewski
::
:: Received November 30, 1990
:: Copyright (c) 1990-2021 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 ));