theorem :: TOPS_4:22

for T being non empty TopSpace
for f being Function of R^1,T holds
( f is continuous iff for p being Point of R^1
for V being open Subset of T st f . p in V holds
ex s being positive Real st f .: ].(p - s),(p + s).[ c= V )