reconsider n = n as Element of NAT by ORDINAL1:def 12;

reconsider Y = (-) X as Subset of (TOP-REAL n) ;

for p being Point of (TOP-REAL n) st p in Y holds

ex r being positive Real st Ball (p,r) c= Y_{1} being Subset of (TOP-REAL n) st b_{1} = (-) X holds

b_{1} is open
by TOPS_4:2; :: thesis: verum

reconsider Y = (-) X as Subset of (TOP-REAL n) ;

for p being Point of (TOP-REAL n) st p in Y holds

ex r being positive Real st Ball (p,r) c= Y

proof

hence
for b
let p be Point of (TOP-REAL n); :: thesis: ( p in Y implies ex r being positive Real st Ball (p,r) c= Y )

assume p in Y ; :: thesis: ex r being positive Real st Ball (p,r) c= Y

then - p in (-) Y by Def3;

then consider r being positive Real such that

A1: Ball ((- p),r) c= X by TOPS_4:2;

take r ; :: thesis: Ball (p,r) c= Y

let x be Element of (TOP-REAL n); :: according to LATTICE7:def 1 :: thesis: ( not x in Ball (p,r) or x in Y )

assume x in Ball (p,r) ; :: thesis: x in Y

then - x in Ball ((- p),r) by Th23;

hence x in Y by A1, Th24; :: thesis: verum

end;assume p in Y ; :: thesis: ex r being positive Real st Ball (p,r) c= Y

then - p in (-) Y by Def3;

then consider r being positive Real such that

A1: Ball ((- p),r) c= X by TOPS_4:2;

take r ; :: thesis: Ball (p,r) c= Y

let x be Element of (TOP-REAL n); :: according to LATTICE7:def 1 :: thesis: ( not x in Ball (p,r) or x in Y )

assume x in Ball (p,r) ; :: thesis: x in Y

then - x in Ball ((- p),r) by Th23;

hence x in Y by A1, Th24; :: thesis: verum

b