:: deftheorem defines continuous FINTOPO8:def 7 :
for NTX, NTY being NTopSpace
for f being Function of NTX,NTY holds
( f is continuous iff for x being Point of NTX holds f is_continuous_at x );