let AFP be AffinPlane; :: thesis: ( AFP is Desarguesian implies 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 ) )
assume A1: AFP is Desarguesian ; :: 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 )
let o, a, b be Element of AFP; :: thesis: ( o <> a & o <> b & LIN o,a,b implies ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) )
assume A2: ( o <> a & o <> b & LIN o,a,b ) ; :: thesis: ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b )
then consider f being Permutation of the carrier of AFP such that
A3: for x, y being Element of AFP 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 AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,x // p',y & LIN o,a,y ) ) ) ) by A1, Lm13;
( f is dilatation & f . o = o & f . a = b ) by A1, A2, A3, Lm17;
hence ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) ; :: thesis: verum