let X be RealNormSpace; :: thesis: for y1 being Point of X
for r being real number holds Ball y1,r = y1 + (Ball (0. X),r)
let y1 be Point of X; :: thesis: for r being real number holds Ball y1,r = y1 + (Ball (0. X),r)
let r be real number ; :: thesis: Ball y1,r = y1 + (Ball (0. X),r)
thus Ball y1,r c= y1 + (Ball (0. X),r) :: according to XBOOLE_0:def 10 :: thesis: y1 + (Ball (0. X),r) c= Ball y1,r

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in Ball y1,r or t in y1 + (Ball (0. X),r) )
assume A1: t in Ball y1,r ; :: thesis: t in y1 + (Ball (0. X),r)
reconsider z1 = t as Point of X by A1;
set z0 = z1 - y1;
ex zz1 being Point of X st
( z1 = zz1 & ||.(y1 - zz1).|| < r ) by A1;
then ||.(- (z1 - y1)).|| < r by RLVECT_1:47;
then ||.((0. X) - (z1 - y1)).|| < r by RLVECT_1:27;
then A2: z1 - y1 in Ball (0. X),r ;
(z1 - y1) + y1 = z1 + ((- y1) + y1) by RLVECT_1:def 6;
then (z1 - y1) + y1 = z1 + (0. X) by RLVECT_1:16;
then z1 = (z1 - y1) + y1 by RLVECT_1:10;
hence t in y1 + (Ball (0. X),r) by A2; :: thesis: verum

end;

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in y1 + (Ball (0. X),r) or t in Ball y1,r )
assume t in y1 + (Ball (0. X),r) ; :: thesis: t in Ball y1,r
then consider z0 being Point of X such that
B1: ( t = y1 + z0 & z0 in Ball (0. X),r ) ;
set z1 = z0 + y1;
ex zz0 being Point of X st
( z0 = zz0 & ||.((0. X) - zz0).|| < r ) by B1;
then ||.(- z0).|| < r by RLVECT_1:27;
then ||.z0.|| < r by NORMSP_1:6;
then ||.(z0 + (0. X)).|| < r by RLVECT_1:10;
then ||.(z0 + (y1 + (- y1))).|| < r by RLVECT_1:16;
then ||.((z0 + y1) - y1).|| < r by RLVECT_1:def 6;
then ||.(y1 - (z0 + y1)).|| < r by NORMSP_1:11;
hence t in Ball y1,r by B1; :: thesis: verum