for f being PartFunc of REAL,REAL
for x0 being Real holds
( f is_continuous_in x0 iff for N1 being Neighbourhood of f . x0 ex N being Neighbourhood of x0 st
for x1 being Real st x1 in dom f & x1 in N holds
f . x1 in N1 )