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