for AFP being AffinPlane
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 )