for X, Y being non empty TopSpace
for f being Function of X,Y
for x being Point of X holds
( f is_continuous_at x iff for G being a_neighborhood of f . x holds f " G is a_neighborhood of x )