theorem :: TRANSGEO:97

for AFP being AffinPlane
for K being Subset of AFP
for p being Element of AFP
for f being Permutation of the carrier of AFP st f is collineation & K is being_line & ( for x being Element of AFP st x in K holds
f . x = x ) & not p in K & f . p = p holds
f = id the carrier of AFP