:: deftheorem defines is_continuous FINTOPO4:def 2 :
for FT1, FT2 being non empty RelStr
for f being Function of FT1,FT2
for n being Nat holds
( f is_continuous n iff for x being Element of FT1
for y being Element of FT2 st x in the carrier of FT1 & y = f . x holds
f .: (U_FT (x,0)) c= U_FT (y,n) );