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 for x, y being Point of (Euclid n) st x in pA & y in pA holds
dist (x,y) <= rlet x,
y be
Point of
(Euclid n);
( x in pA & y in pA implies dist (x,y) <= r )assume
x in pA
;
( 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
;
dist (x,y) <= rthen 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;
verum end;
then
pA is bounded
by A1, TBSP_1:def 7;
hence
p + A is bounded
by JORDAN2C:11; verum