:: deftheorem Def6 defines translation EUCLMETR:def 6 :
for IT being OrtAfSp holds
( IT is translation iff AffinStruct(# the carrier of IT, the CONGR of IT #) is translational );