:: deftheorem defines is_Sc HOMOTHET:def 1 :
for AFP being AffinPlane
for f being Permutation of the carrier of AFP
for K being Subset of AFP holds
( f is_Sc K iff ( f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & ( for x being Element of AFP holds x,f . x // K ) ) );