:: deftheorem Def10 defines transl RLTOPSP1:def 10 :
for X being non empty RLTopStruct
for a being Point of X
for b₃ being Function of X,X holds
( b₃ = transl (a,X) iff for x being Point of X holds b₃ . x = a + x );