:: deftheorem Def5 defines translation PAPDESAF:def 5 :
for IT being OAffinSpace holds
( IT is translation iff Lambda IT is translational );