begin
Lm1:
for AFP being AffinPlane holds
( AFP is Desarguesian iff for o, a, a', p, p', q, q' being Element of st LIN o,a,a' & LIN o,p,p' & LIN o,q,q' & not LIN o,a,p & not LIN o,a,q & a,p // a',p' & a,q // a',q' holds
p,q // p',q' )
Lm2:
for AFP being AffinPlane holds
( AFP is Moufangian iff for o being Element of
for K being Subset of
for c, c', a, b, a', b' being Element of st o in K & c in K & c' in K & K is being_line & LIN o,a,a' & LIN o,b,b' & not a in K & a,b // K & a',b' // K & a,c // a',c' holds
b,c // b',c' )
Lm3:
for AFP being AffinPlane st AFP is Moufangian holds
for K being Subset of
for o, a, b, c, a', b', c' being Element of st K is being_line & o in K & c in K & c' in K & not a in K & a <> b & LIN o,a,a' & a,b // a',b' & b,c // b',c' & a,c // a',c' & a,b // K holds
LIN o,b,b'
Lm4:
for AFP being AffinPlane st AFP is Moufangian holds
for K, A, C being Subset of
for p, q, a, a', b, b' being Element of st K // A & K // C & K <> A & K <> C & p in K & q in K & a in A & a' in A & b in C & b' in C & p,a // q,a' & p,b // q,b' holds
a,b // a',b'
theorem Th1:
for
AFP being
AffinPlane for
o,
a,
p,
b,
x,
y,
p',
q,
q' being
Element of st not
LIN o,
a,
p &
LIN o,
a,
b &
LIN o,
a,
x &
LIN o,
a,
y &
LIN o,
p,
p' &
LIN o,
p,
q &
LIN o,
p,
q' &
p <> q &
o <> q &
o <> x &
a,
p // b,
p' &
a,
q // b,
q' &
x,
p // y,
p' &
AFP is
Desarguesian holds
x,
q // y,
q'
theorem Th2:
Lm5:
for AFP being AffinPlane
for o, a, b, y, x being Element of st o <> a & o <> b & LIN o,a,b & LIN o,a,y & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) holds
LIN o,a,x
Lm6:
for AFP being AffinPlane
for o, a, b, x, y being Element of st o <> a & o <> b & LIN o,a,b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) holds
( o <> b & o <> a & LIN o,b,a & ( ( not LIN o,b,y & LIN o,y,x & b,y // a,x ) or ( LIN o,b,y & ex p, p' being Element of st
( not LIN o,b,p & LIN o,p,p' & b,p // a,p' & p,y // p',x & LIN o,b,x ) ) ) )
Lm7:
for AFP being AffinPlane
for o, a, x, y, b being Element of st o <> a & x = o & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) holds
y = o
Lm8:
for AFP being AffinPlane
for o, a, b, x being Element of st o <> a & LIN o,a,b holds
ex y being Element of st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) )
Lm9:
for AFP being AffinPlane
for o, a, b, y being Element of st o <> a & o <> b & LIN o,a,b holds
ex x being Element of st
( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) )
Lm10:
for AFP being AffinPlane
for o, a, b, x, y being Element of st o <> a & a = b & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) holds
x = y
Lm11:
for AFP being AffinPlane
for o, a, b, x, y, r being Element of st o <> a & LIN o,a,b & AFP is Desarguesian & LIN o,a,x & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',r & LIN o,a,r ) holds
y = r
Lm12:
for AFP being AffinPlane
for o, a, b, x, y, r being Element of st o <> a & o <> b & LIN o,a,b & AFP is Desarguesian & ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) & ( ( not LIN o,a,r & LIN o,r,y & a,r // b,y ) or ( LIN o,a,r & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,r // p',y & LIN o,a,y ) ) ) holds
x = r
Lm13:
for AFP being AffinPlane
for o, a, b being Element of st AFP is Desarguesian & o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
for x, y being Element of holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) )
Lm14:
for AFP being AffinPlane
for o, a, b, x, y, z, t being Element of st AFP is Desarguesian & o <> a & LIN o,a,b & not LIN o,a,x & LIN o,x,y & a,x // b,y & LIN o,a,z & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,z // p',t & LIN o,a,t ) holds
x,z // y,t
Lm15:
for AFP being AffinPlane
for o, a, b, x, y, z, t being Element of st AFP is Desarguesian & o <> a & LIN o,a,b & LIN o,a,x & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) & not LIN o,a,z & LIN o,z,t & a,z // b,t holds
x,z // y,t
Lm16:
for AFP being AffinPlane
for o, a, x, b, y, z, t being Element of st o <> a & LIN o,a,x & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) & LIN o,a,z & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,z // p',t & LIN o,a,t ) holds
x,z // y,t
Lm17:
for AFP being AffinPlane
for o, a, b being Element of
for f being Permutation of the carrier of AFP st o <> a & LIN o,a,b & AFP is Desarguesian & ( for x, y being Element of holds
( f . x = y iff ( ( not LIN o,a,x & LIN o,x,y & a,x // b,y ) or ( LIN o,a,x & ex p, p' being Element of st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) ) ) holds
( f is dilatation & f . o = o & f . a = b )
theorem Th3:
theorem
:: deftheorem Def1 defines is_Sc HOMOTHET:def 1 :
theorem Th5:
theorem Th6:
Lm18:
for AFP being AffinPlane
for a, b, x, y being Element of
for K being Subset of st a,b // K & not a in K & ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) holds
( b,a // K & not b in K & ( ( y in K & y = x ) or ( not y in K & ex p, p' being Element of st
( p in K & p' in K & p,b // p',y & p,a // p',x & y,x // K ) ) ) )
Lm19:
for AFP being AffinPlane
for a, b being Element of
for K being Subset of st a,b // K & not a in K holds
for x being Element of ex y being Element of st
( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) )
Lm20:
for AFP being AffinPlane
for a, b being Element of
for K being Subset of st a,b // K & not a in K holds
for y being Element of ex x being Element of st
( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) )
theorem Th7:
for
AFP being
AffinPlane for
p,
q,
p',
q',
a,
b,
x,
y being
Element of
for
K,
M being
Subset of st
K // M &
p in K &
q in K &
p' in K &
q' in K &
AFP is
Moufangian &
a in M &
b in M &
x in M &
y in M &
a <> b &
q <> p &
p,
a // p',
x &
p,
b // p',
y &
q,
a // q',
x holds
q,
b // q',
y
Lm21:
for AFP being AffinPlane
for a, b, x, p, p', y, q, q' being Element of
for K being Subset of st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K & q in K & q' in K & q,a // q',x holds
q,b // q',y
Lm22:
for AFP being AffinPlane
for a, b, x, p, p', y, q, q', s being Element of
for K being Subset of st a,b // K & not a in K & not x in K & AFP is Moufangian & p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K & q in K & q' in K & q,a // q',x & x,s // K & q,b // q',s holds
s = y
Lm23:
for AFP being AffinPlane
for a, b, x, y, r being Element of
for K being Subset of st a,b // K & not a in K & AFP is Moufangian & ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) & ( ( r in K & r = y ) or ( not r in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',r & p,b // p',y & r,y // K ) ) ) holds
x = r
Lm24:
for AFP being AffinPlane
for a, b being Element of
for K being Subset of st a,b // K & not a in K & AFP is Moufangian holds
ex f being Permutation of the carrier of AFP st
for x, y being Element of holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) )
Lm25:
for AFP being AffinPlane
for a, b being Element of
for K being Subset of
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ) ) holds
f . a = b
Lm26:
for AFP being AffinPlane
for a, b being Element of
for K being Subset of
for f being Permutation of the carrier of AFP st a,b // K & ( for x, y being Element of holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ) ) holds
for x being Element of holds x,f . x // K
Lm27:
for AFP being AffinPlane
for a, b being Element of
for K being Subset of
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ) ) holds
f is collineation
Lm28:
for AFP being AffinPlane
for a, b being Element of
for K being Subset of
for f being Permutation of the carrier of AFP st a,b // K & not a in K & ( for x, y being Element of holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ) ) holds
f is_Sc K
theorem Th8:
theorem