theorem :: TOPS_4:18

for m being Nat
for T being non empty TopSpace
for f being Function of T,(TOP-REAL m) holds
( f is continuous iff for p being Point of T
for r being positive Real ex W being open Subset of T st
( p in W & f .: W c= Ball ((f . p),r) ) )