let X be RealNormSpace; 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; for r being Real holds Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))
let r be Real; Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))
thus
Ball ((0. X),r) c= (- 1) * (Ball ((0. X),r))
XBOOLE_0:def 10 (- 1) * (Ball ((0. X),r)) c= Ball ((0. X),r)
let z be object ; TARSKI:def 3 ( not z in (- 1) * (Ball ((0. X),r)) or z in Ball ((0. X),r) )
assume A3:
z in (- 1) * (Ball ((0. X),r))
; 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; verum