let AFP be AffinPlane; :: thesis: for a, b being Element of AFP
for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
for x being Element of AFP holds x,f . x // K
let a, b be Element of AFP; :: thesis: for K being Subset of AFP
for f being Permutation of the carrier of AFP st a,b // K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
for x being Element of AFP holds x,f . x // K
let K be Subset of AFP; :: thesis: for f being Permutation of the carrier of AFP st a,b // K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) holds
for x being Element of AFP holds x,f . x // K
let f be Permutation of the carrier of AFP; :: thesis: ( a,b // K & ( for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ) implies for x being Element of AFP holds x,f . x // K )
assume that
A1: a,b // K and
A2: for x, y being Element of AFP holds
( f . x = y iff ( ( x in K & x = y ) or ( not x in K & ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,y & x,y // K ) ) ) ) ; :: thesis: for x being Element of AFP holds x,f . x // K
let x be Element of AFP; :: thesis: x,f . x // K
set y = f . x;
A3: K is being_line by A1, AFF_1:26;
A4: now :: thesis: ( x in K implies x,f . x // K )
assume x in K ; :: thesis: x,f . x // K
then f . x = x by A2;
hence x,f . x // K by A3, AFF_1:33; :: thesis: verum
end;
now :: thesis: ( not x in K implies x,f . x // K )
assume not x in K ; :: thesis: x,f . x // K
then ex p, p9 being Element of AFP st
( p in K & p9 in K & p,a // p9,x & p,b // p9,f . x & x,f . x // K ) by A2;
hence x,f . x // K ; :: thesis: verum
end;
hence x,f . x // K by A4; :: thesis: verum