let AFP be AffinPlane; :: thesis: for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b )
let a, b be Element of AFP; :: thesis: for K being Subset of AFP st a,b // K & not a in K & AFP is Moufangian holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b )
let K be Subset of AFP; :: thesis: ( a,b // K & not a in K & AFP is Moufangian implies ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b ) )
assume that
A1: a,b // K and
A2: not a in K and
A3: AFP is Moufangian ; :: thesis: ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b )
consider f being Permutation of the carrier of AFP such that
A4: 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 ) ) ) ) by A1, A2, A3, Lm24;
A5: f . a = b by A1, A2, A4, Lm25;
f is_Sc K by A1, A2, A4, Lm28;
hence ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b ) by A5; :: thesis: verum