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

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Ball (0. X),r or z in (- 1) * (Ball (0. X),r) )
assume R1: z in Ball (0. X),r ; :: thesis: z in (- 1) * (Ball (0. X),r)
then reconsider z1 = z as Point of X ;
ex zz1 being Point of X st
( z1 = zz1 & ||.((0. X) - zz1).|| < r ) by R1;
then ||.(- z1).|| < r by RLVECT_1:27;
then ||.(- (- z1)).|| < r by NORMSP_1:6;
then ||.((0. X) - (- z1)).|| < r by RLVECT_1:27;
then R3: - z1 in Ball (0. X),r ;
(- 1) * (- z1) = 1 * z1 by RLVECT_1:40
.= z1 by RLVECT_1:def 9 ;
hence z in (- 1) * (Ball (0. X),r) by R3; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in (- 1) * (Ball (0. X),r) or z in Ball (0. X),r )
assume R1: z in (- 1) * (Ball (0. X),r) ; :: thesis: z in Ball (0. X),r
then reconsider z1 = z as Point of X ;
consider y1 being Point of X such that
B1: ( z1 = (- 1) * y1 & y1 in Ball (0. X),r ) by R1;
ex zz1 being Point of X st
( y1 = zz1 & ||.((0. X) - zz1).|| < r ) by B1;
then ||.(- y1).|| < r by RLVECT_1:27;
then ||.(- (- y1)).|| < r by NORMSP_1:6;
then R3: ||.((0. X) - (- y1)).|| < r by RLVECT_1:27;
- y1 = z1 by B1, RLVECT_1:29;
hence z in Ball (0. X),r by R3; :: thesis: verum