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 & AFP is Moufangian & ( 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 is_Sc 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 & not a in K & AFP is Moufangian & ( 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 is_Sc K
let K be Subset of AFP; :: thesis: for f being Permutation of the carrier of AFP st a,b // K & not a in K & AFP is Moufangian & ( 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 is_Sc K
let f be Permutation of the carrier of AFP; :: thesis: ( a,b // K & not a in K & AFP is Moufangian & ( 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 is_Sc K )
assume that
A1: ( a,b // K & not a in K ) and
A2: AFP is Moufangian and
A3: 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 is_Sc K
A4: K is being_line by A1, AFF_1:40;
A5: f is collineation by A1, A2, A3, Lm27;
A6: for x being Element of AFP st x in K holds
f . x = x by A3;
for x being Element of AFP holds x,f . x // K by A1, A3, Lm26;
hence f is_Sc K by A4, A5, A6, Def1; :: thesis: verum