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 & not a in 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, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ) ) holds
f . a = b
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 & not a in 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, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ) ) holds
f . a = b
let K be Subset of AFP; :: thesis: for f being Permutation of the carrier of AFP st a,b // K & not a in 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, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ) ) holds
f . a = b
let f be Permutation of the carrier of AFP; :: thesis: ( a,b // K & not a in 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, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ) ) implies f . a = b )
assume A1: ( a,b // K & not a in K ) ; :: thesis: ( ex x, y being Element of AFP st
( ( not f . x = y or ( x in K & x = y ) or ( not x in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) implies ( ( ( x in K & x = y ) or ( not x in K & ex p, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) & not f . x = y ) ) or f . a = b )
assume 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, p' being Element of AFP st
( p in K & p' in K & p,a // p',x & p,b // p',y & x,y // K ) ) ) ) ; :: thesis: f . a = b
K is being_line by A1, AFF_1:40;
then consider p, q being Element of AFP such that
A3: ( p in K & q in K & p <> q ) by AFF_1:31;
( p,a // p,a & p,b // p,b ) by AFF_1:11;
hence f . a = b by A1, A2, A3; :: thesis: verum