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 real positive number st Ball (p,r) c= Y

proof

let p be Point of (TOP-REAL n); :: thesis: ( p in Y implies ex r being real positive number st Ball (p,r) c= Y )
assume p in Y ; :: thesis: ex r being real positive number st Ball (p,r) c= Y
then - p in (-) Y by Def3;
then consider r being real positive number 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;

hence for b₁ being Subset of (TOP-REAL n) st b₁ = (-) X holds
b₁ is open by TOPS_4:2; :: thesis: verum