:: deftheorem defines is_continuous_at TMAP_1:def 2 :
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 ex H being a_neighborhood of x st f .: H c= G );