begin
definition
let AS be
AffinSpace;
attr AS is
Fanoian means :
Def1:
for
a,
b,
c,
d being
Element of
AS st
a,
b // c,
d &
a,
c // b,
d &
a,
d // b,
c holds
LIN a,
b,
c;
end;
::
deftheorem Def1 defines
Fanoian TRANSLAC:def 1 :
for AS being AffinSpace holds
( AS is Fanoian iff for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
LIN a,b,c );
Lm1:
for AS being AffinSpace
for a, b, c, p being Element of AS st LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p holds
ex x being Element of AS st
( LIN p,a,x & p <> x & a <> x )
Lm2:
for AS being AffinSpace
for a, b, c, p, q being Element of AS st LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p & LIN a,b,q holds
ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )
Lm3:
for AS being AffinSpace
for a, b, c, p, q being Element of AS st LIN a,b,c & a <> b & a <> c & b <> c & not LIN a,b,p & p,q // a,b holds
ex x being Element of AS st
( LIN p,q,x & p <> x & q <> x )
theorem Th2:
for
AFP being
AffinPlane for
a,
b,
c,
d being
Element of
AFP st
AFP is
Fanoian &
a,
b // c,
d &
a,
c // b,
d & not
LIN a,
b,
c holds
ex
p being
Element of
AFP st
(
LIN b,
c,
p &
LIN a,
d,
p )
Lm4:
for AFP being AffinPlane
for a, b, x, y being Element of AFP st not LIN a,b,x & a,b // x,y & x <> y holds
( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b )
Lm5:
for AFP being AffinPlane
for a, b, x, y being Element of AFP st not LIN a,b,x & a,b // x,y & a,x // b,y holds
( not LIN x,y,a & not LIN b,a,y & not LIN y,x,b )
theorem Th4:
for
AFP being
AffinPlane holds
(
AFP is
translational iff for
a,
a9,
b,
c,
b9,
c9 being
Element of
AFP st not
LIN a,
a9,
b & not
LIN a,
a9,
c &
a,
a9 // b,
b9 &
a,
a9 // c,
c9 &
a,
b // a9,
b9 &
a,
c // a9,
c9 holds
b,
c // b9,
c9 )
Lm6:
for AFP being AffinPlane
for a, b, x being Element of AFP st a <> b holds
ex y being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) )
Lm7:
for AFP being AffinPlane
for a, b, y being Element of AFP st a <> b holds
ex x being Element of AFP st
( ( not LIN a,b,x & a,b // x,y & a,x // b,y ) or ( LIN a,b,x & ex p, q being Element of AFP st
( not LIN a,b,p & a,b // p,q & a,p // b,q & p,q // x,y & p,x // q,y ) ) )
Lm8:
for AFP being AffinPlane
for a, b, x, p, q, p9, q9, y, y9 being Element of AFP st AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p // b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9 & not LIN a,b,p & not LIN a,b,p9 & not LIN p,q,p9 holds
y = y9
theorem Th6:
for
AFP being
AffinPlane for
a,
b,
p,
q being
Element of
AFP st ( for
p,
q,
r being
Element of
AFP st
p <> q &
LIN p,
q,
r & not
r = p holds
r = q ) &
a,
b // p,
q &
a,
p // b,
q & not
LIN a,
b,
p holds
a,
q // b,
p
Lm9:
for AFP being AffinPlane
for a, b, x, p, q, p9, q9, y, y9 being Element of AFP st AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p // b,q & a,p9 // b,q9 & p,q // x,y & p9,q9 // x,y9 & p,x // q,y & p9,x // q9,y9 & not LIN a,b,p & not LIN a,b,p9 holds
y = y9
Lm10:
for AFP being AffinPlane
for a, b, x, p, q, y being Element of AFP st a <> b & LIN a,b,x & a,b // p,q & a,p // b,q & p,q // x,y & not LIN a,b,p holds
( p <> q & LIN a,b,y )
Lm11:
for AFP being AffinPlane
for a, b, x, p, q, p9, q9, y, x9 being Element of AFP st AFP is translational & a <> b & LIN a,b,x & a,b // p,q & a,b // p9,q9 & a,p // b,q & a,p9 // b,q9 & p,q // x,y & p,x // q,y & p9,q9 // x9,y & p9,x9 // q9,y & not LIN a,b,p & not LIN a,b,p9 holds
x = x9
Lm12:
for AFP being AffinPlane
for a, b being Element of AFP st AFP is translational & a <> b holds
ex f being Permutation of the carrier of AFP st
( f is translation & f . a = b )