theorem :: TOPS_4:25

for m being Nat
for f being Function of R^1,(TOP-REAL m) holds
( f is continuous iff for p being Point of R^1
for r being positive Real ex s being positive Real st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) )