:: deftheorem defines is_continuous_at FINTOPO8:def 6 :
for NTX, NTY being NTopSpace
for f being Function of NTX,NTY
for x being Point of NTX holds
( f is_continuous_at x iff for F being Filter of the carrier of NTX st x in lim_filter F holds
f . x in lim_filter (f,F) );