for AFP being AffinPlane holds
( AFP is Desarguesian iff 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 ) ) by Th2, Th3;