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

let p be Point of (TOP-REAL n); :: thesis:
assume p in Y ; :: thesis:
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:
let x be Element of (TOP-REAL n); :: according to LATTICE7:def 1 :: thesis:
assume x in Ball (p,r) ; :: thesis:
then - x in Ball ((- p),r) by Th23;
hence x in Y by A1, Th24; :: thesis:

end;

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