:: deftheorem defines collineation TRANSGEO:def 12 :
for AFS being AffinSpace
for f being Permutation of the carrier of AFS holds
( f is collineation iff f is_automorphism_of the CONGR of AFS );