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 that
A2: o <> a and
A3: o <> b and
A4: LIN o,a,b ; :: thesis: ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b )
consider f being Permutation of the carrier of AFP such that
A5: 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, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,x // p9,y & LIN o,a,y ) ) ) ) by A1, A2, A3, A4, Lm13;
A6: f . a = b by A1, A2, A4, A5, Lm17;
A7: f . o = o by A1, A2, A4, A5, Lm17;
f is dilatation by A1, A2, A4, A5, Lm17;
hence ex f being Permutation of the carrier of AFP st
( f is dilatation & f . o = o & f . a = b ) by A7, A6; :: thesis: verum