let AFP be AffinPlane; :: thesis:
let o, a, b be Element of AFP; :: thesis:
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, p' being Element of AFP st
( not LIN o,a,p & LIN o,p,p' & a,p // b,p' & p,$1 // p',$2 & LIN o,a,$2 ) ) );
assume A1: ( AFP is Desarguesian & o <> a & o <> b & LIN o,a,b ) ; :: thesis:
then A2: for x being Element of AFP ex y being Element of AFP st S₁[x,y] by Lm8;
A3: for y being Element of AFP ex x being Element of AFP st S₁[x,y] by A1, Lm9;
A4: for x, y, r being Element of AFP st S₁[x,y] & S₁[r,y] holds
x = r by A1, Lm12;
A5: for x, y, s being Element of AFP st S₁[x,y] & S₁[x,s] holds
y = s by A1, Lm11, AFF_1:70;
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(A2, A3, A4, A5);
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, 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 ) ) ) ) ; :: thesis: