:: deftheorem Def6 defines translatible VECTMETR:def 6 :
for V being non empty RLSMetrStruct holds
( V is translatible iff for u, w, v being Element of V holds dist (v,w) = dist ((v + u),(w + u)) );