set TR = TOP-REAL n;
set En = Euclid n;
reconsider a = A as bounded Subset of (Euclid n) by JORDAN2C:11;
reconsider pA = p + A as Subset of (Euclid n) by EUCLID:67;
consider r being Real such that
A1: 0 < r and
A2: for x, y being Point of (Euclid n) st x in a & y in a holds
dist (x,y) <= r by TBSP_1:def 7;
A3: pA = { (p + u) where u is Element of (TOP-REAL n) : u in A } by RUSUB_4:def 8;

now :: thesis: for x, y being Point of (Euclid n) st x in pA & y in pA holds
dist (x,y) <= r

let x, y be Point of (Euclid n); :: thesis: ( x in pA & y in pA implies dist (x,y) <= r )
assume x in pA ; :: thesis: ( y in pA implies dist (x,y) <= r )
then consider px being Element of (TOP-REAL n) such that
A4: x = p + px and
A5: px in A by A3;
assume y in pA ; :: thesis: dist (x,y) <= r
then consider py being Element of (TOP-REAL n) such that
A6: y = p + py and
A7: py in A by A3;
reconsider pX = px, pY = py as Point of (Euclid n) by EUCLID:67;
(p + px) - (p + py) = ((p + px) - p) - py by RLVECT_1:27
.= px - py by RLVECT_4:1 ;
then dist (x,y) = |.(px - py).| by A4, A6, SPPOL_1:39
.= dist (pX,pY) by SPPOL_1:39 ;
hence dist (x,y) <= r by A2, A5, A7; :: thesis: verum

end;

then pA is bounded by A1, TBSP_1:def 7;
hence p + A is bounded by JORDAN2C:11; :: thesis: verum