:: deftheorem defines translation TRANSGEO:def 11 :
for AFS being AffinSpace
for f being Permutation of the carrier of AFS holds
( f is translation iff ( f is dilatation & ( f = id the carrier of AFS or for a being Element of AFS holds a <> f . a ) ) );