let AFP be AffinPlane; :: thesis: ( ( 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 ) ; :: thesis: AFP is Desarguesian

now :: thesis: 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,q9

let o, a, a9, p, p9, q, q9 be Element of AFP; :: thesis: ( 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 ; :: thesis: p,q // p9,q9

A9: now :: thesis: ( o <> a9 implies p,q // p9,q9 )

assume A10: o <> a9 ; :: thesis: 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; :: thesis: verum

end;

now :: thesis: ( o = a9 implies p,q // p9,q9 )

assume A17: o = a9 ; :: thesis: p,q // p9,q9
then 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; :: thesis: verum

end;

hence p,q // p9,q9 by A9; :: thesis: verum

end;

hence AFP is Desarguesian by Lm1; :: thesis: verum