:: deftheorem defines continuous CC0SP2:def 1 :
for X being TopStruct
for f being Function of the carrier of X,COMPLEX holds
( f is continuous iff for Y being Subset of COMPLEX st Y is closed holds
f " Y is closed );