theorem :: TOPS_4:9

for n, m being Nat
for f being Function of (TOP-REAL m),(TOP-REAL n) holds
( f is open iff for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st Ball ((f . p),s) c= f .: (Ball (p,r)) )