for T being non empty TopSpace
for f being Function of T,R^1
for x being Point of T holds
( f is_continuous_at x iff for e being Real st e > 0 holds
ex H being Subset of T st
( H is open & x in H & ( for y being Point of T st y in H holds
|.((f . y) - (f . x)).| < e ) ) )