theorem :: FINTOPO8:16

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 f is_continuous_at x & y = f . x holds
for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V by Lm11;