for m being Nat
for P being Subset of (TOP-REAL m) holds
( P is open iff for p being Point of (TOP-REAL m) st p in P holds
ex r being positive Real st Ball (p,r) c= P )