let AFP be AffinPlane; :: thesis: for o, a, b being Element of AFP st AFP is Desarguesian & o <> a & o <> b & LIN o,a,b holds
ex f being Permutation of the carrier of AFP st
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 ) ) ) )
let o, a, b be Element of AFP; :: thesis: ( AFP is Desarguesian & o <> a & o <> b & LIN o,a,b implies ex f being Permutation of the carrier of AFP st
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 ) ) ) ) )
defpred S₁[ Element of AFP, Element of AFP] means ( ( not LIN o,a,$1 & LIN o,$1,$2 & a,$1 // b,$2 ) or ( LIN o,a,$1 & ex p, p9 being Element of AFP st
( not LIN o,a,p & LIN o,p,p9 & a,p // b,p9 & p,$1 // p9,$2 & LIN o,a,$2 ) ) );
assume that
A1: AFP is Desarguesian and
A2: o <> a and
A3: o <> b and
A4: LIN o,a,b ; :: thesis: ex f being Permutation of the carrier of AFP st
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 ) ) ) )
A5: for y being Element of AFP ex x being Element of AFP st S₁[x,y] by A2, A3, A4, Lm9;
A6: for x being Element of AFP ex y being Element of AFP st S₁[x,y] by A2, A4, Lm8;
A7: for x, y, s being Element of AFP st S₁[x,y] & S₁[x,s] holds
y = s by A1, A2, A4, Lm11, AFF_1:56;
A8: for x, y, r being Element of AFP st S₁[x,y] & S₁[r,y] holds
x = r by A1, A2, A3, A4, Lm12;
ex f being Permutation of the carrier of AFP st
for x, y being Element of AFP holds
( f . x = y iff S₁[x,y] ) from TRANSGEO:sch 1(A6, A5, A8, A7);
hence ex f being Permutation of the carrier of AFP st
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 ) ) ) ) ; :: thesis: verum