:: Elementary Variants of Affine Configurational Theorems
:: by Krzysztof Pra\.zmowski and Krzysztof Radziszewski
::
:: Received November 30, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: PARDEPAP:1
for
SAS being
AffinPlane st
SAS is
Pappian holds
for
a1,
a2,
a3,
b1,
b2,
b3 being
Element of
SAS st
a1,
a2 // a1,
a3 &
b1,
b2 // b1,
b3 &
a1,
b2 // a2,
b1 &
a2,
b3 // a3,
b2 holds
a3,
b1 // a1,
b3
theorem Th2: :: PARDEPAP:2
for
SAS being
AffinPlane st
SAS is
Desarguesian holds
for
o,
a,
a',
b,
b',
c,
c' being
Element of
SAS st 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' holds
b,
c // b',
c'
theorem Th3: :: PARDEPAP:3
for
SAS being
AffinPlane st
SAS is
translational holds
for
a,
a',
b,
b',
c,
c' being
Element of
SAS st 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' holds
b,
c // b',
c'
theorem :: PARDEPAP:4
canceled;
theorem :: PARDEPAP:5
ex
SAS being
AffinPlane st
( ( for
o,
a,
a',
b,
b',
c,
c' being
Element of
SAS st 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' holds
b,
c // b',
c' ) & ( for
a,
a',
b,
b',
c,
c' being
Element of
SAS st 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' holds
b,
c // b',
c' ) & ( for
a1,
a2,
a3,
b1,
b2,
b3 being
Element of
SAS st
a1,
a2 // a1,
a3 &
b1,
b2 // b1,
b3 &
a1,
b2 // a2,
b1 &
a2,
b3 // a3,
b2 holds
a3,
b1 // a1,
b3 ) & ( for
a,
b,
c,
d being
Element of
SAS st not
a,
b // a,
c &
a,
b // c,
d &
a,
c // b,
d holds
not
a,
d // b,
c ) )
theorem :: PARDEPAP:6
for
SAS being
AffinPlane for
o,
a being
Element of
SAS 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 ) ) )