let AFP be AffinPlane; ( ( for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) ) implies AFP is Desarguesian )
assume A1:
for o, a, b being Element of AFP st o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b )
; AFP is Desarguesian
now for o, a, a9, p, p9, q, q9 being Element of AFP st LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 holds
p,q // p9,q9let o,
a,
a9,
p,
p9,
q,
q9 be
Element of
AFP;
( LIN o,a,a9 & LIN o,p,p9 & LIN o,q,q9 & not LIN o,a,p & not LIN o,a,q & a,p // a9,p9 & a,q // a9,q9 implies p,q // p9,q9 )assume that A2:
LIN o,
a,
a9
and A3:
LIN o,
p,
p9
and A4:
LIN o,
q,
q9
and A5:
not
LIN o,
a,
p
and A6:
not
LIN o,
a,
q
and A7:
a,
p // a9,
p9
and A8:
a,
q // a9,
q9
;
p,q // p9,q9A9:
now ( o <> a9 implies p,q // p9,q9 )assume A10:
o <> a9
;
p,q // p9,q9
o <> a
by A5, AFF_1:7;
then consider f being
Permutation of the
carrier of
AFP such that A11:
f is
dilatation
and A12:
f . o = o
and A13:
f . a = a9
by A1, A2, A10;
set s =
f . q;
o,
q // o,
f . q
by A11, A12, TRANSGEO:68;
then A14:
LIN o,
q,
f . q
by AFF_1:def 1;
set r =
f . p;
o,
p // o,
f . p
by A11, A12, TRANSGEO:68;
then A15:
LIN o,
p,
f . p
by AFF_1:def 1;
a,
q // a9,
f . q
by A11, A13, TRANSGEO:68;
then A16:
f . q = q9
by A2, A4, A6, A8, A14, AFF_1:56;
a,
p // a9,
f . p
by A11, A13, TRANSGEO:68;
then
f . p = p9
by A2, A3, A5, A7, A15, AFF_1:56;
hence
p,
q // p9,
q9
by A11, A16, TRANSGEO:68;
verum end; now ( o = a9 implies p,q // p9,q9 )assume A17:
o = a9
;
p,q // p9,q9then
o = p9
by A3, A5, A7, AFF_1:55;
then
p9 = q9
by A4, A6, A8, A17, AFF_1:55;
hence
p,
q // p9,
q9
by AFF_1:3;
verum end; hence
p,
q // p9,
q9
by A9;
verum end;
hence
AFP is Desarguesian
by Lm1; verum