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

let o, a, a', p, p', q, q' be Element of AFP; :: thesis: ( 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' implies p,q // p',q' )
assume A2: ( 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' ) ; :: thesis: p,q // p',q'

A3: now

assume A4: o = a' ; :: thesis: p,q // p',q'
then o = p' by A2, AFF_1:69;
then p' = q' by A2, A4, AFF_1:69;
hence p,q // p',q' by AFF_1:12; :: thesis: verum

end;

now

assume A5: o <> a' ; :: thesis: p,q // p',q'
o <> a by A2, AFF_1:16;
then consider f being Permutation of the carrier of AFP such that
A6: ( f is dilatation & f . o = o & f . a = a' ) by A1, A2, A5;
set r = f . p;
set s = f . q;
A7: f . p = p'

proof

( o,p // o,f . p & a,p // a',f . p ) by A6, TRANSGEO:85;
then ( LIN o,p,f . p & a,p // a',f . p ) by AFF_1:def 1;
hence f . p = p' by A2, AFF_1:70; :: thesis: verum

end;

f . q = q'

proof

( o,q // o,f . q & a,q // a',f . q ) by A6, TRANSGEO:85;
then ( LIN o,q,f . q & a,q // a',f . q ) by AFF_1:def 1;
hence f . q = q' by A2, AFF_1:70; :: thesis: verum

end;

hence p,q // p',q' by A6, A7, TRANSGEO:85; :: thesis: verum

end;

hence p,q // p',q' by A3; :: thesis: verum

end;

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