theorem :: FINTOPO8:18

for NTX, NTY being NTopSpace
for x being Point of NTX
for y being Point of NTY
for f being Function of NTX,NTY st y = f . x holds
( f is_continuous_at x iff for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V ) by Lm11, Lm25;