theorem :: HOMOTHET:9

for AFP being AffinPlane holds
( AFP is Moufangian iff for a, b being Element of AFP
for K being Subset of AFP st a,b // K & not a in K holds
ex f being Permutation of the carrier of AFP st
( f is_Sc K & f . a = b ) ) by Th6, Th8;