:: deftheorem defines continuous PSCOMP_1:def 3 :
for T being TopStruct
for f being RealMap of T holds
( f is continuous iff for Y being Subset of REAL st Y is closed holds
f " Y is closed );