let X be RealNormSpace; :: thesis: for x being Point of X

for r being Real holds Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))

let x be Point of X; :: thesis: for r being Real holds Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))

let r be Real; :: 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)

assume A3: 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

A4: z1 = (- 1) * y1 and

A5: y1 in Ball ((0. X),r) by A3;

ex zz1 being Point of X st

( y1 = zz1 & ||.((0. X) - zz1).|| < r ) by A5;

then ||.(- y1).|| < r by RLVECT_1:14;

then ||.(- (- y1)).|| < r by NORMSP_1:2;

then A6: ||.((0. X) - (- y1)).|| < r by RLVECT_1:14;

- y1 = z1 by A4, RLVECT_1:16;

hence z in Ball ((0. X),r) by A6; :: thesis: verum

for r being Real holds Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))

let x be Point of X; :: thesis: for r being Real holds Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))

let r be Real; :: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not z in (- 1) * (Ball ((0. X),r)) or z in Ball ((0. X),r) )
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Ball ((0. X),r) or z in (- 1) * (Ball ((0. X),r)) )

assume A1: 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 A1;

then ||.(- z1).|| < r by RLVECT_1:14;

then ||.(- (- z1)).|| < r by NORMSP_1:2;

then ||.((0. X) - (- z1)).|| < r by RLVECT_1:14;

then A2: - z1 in Ball ((0. X),r) ;

(- 1) * (- z1) = 1 * z1 by RLVECT_1:26

.= z1 by RLVECT_1:def 8 ;

hence z in (- 1) * (Ball ((0. X),r)) by A2; :: thesis: verum

end;assume A1: 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 A1;

then ||.(- z1).|| < r by RLVECT_1:14;

then ||.(- (- z1)).|| < r by NORMSP_1:2;

then ||.((0. X) - (- z1)).|| < r by RLVECT_1:14;

then A2: - z1 in Ball ((0. X),r) ;

(- 1) * (- z1) = 1 * z1 by RLVECT_1:26

.= z1 by RLVECT_1:def 8 ;

hence z in (- 1) * (Ball ((0. X),r)) by A2; :: thesis: verum

assume A3: 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

A4: z1 = (- 1) * y1 and

A5: y1 in Ball ((0. X),r) by A3;

ex zz1 being Point of X st

( y1 = zz1 & ||.((0. X) - zz1).|| < r ) by A5;

then ||.(- y1).|| < r by RLVECT_1:14;

then ||.(- (- y1)).|| < r by NORMSP_1:2;

then A6: ||.((0. X) - (- y1)).|| < r by RLVECT_1:14;

- y1 = z1 by A4, RLVECT_1:16;

hence z in Ball ((0. X),r) by A6; :: thesis: verum