theorem Th2: :: ASCOLI2:2

for S being non empty TopSpace
for T being non empty MetrSpace
for f being Function of S,(TopSpaceMetr T)
for x being Point of S holds
( f is_continuous_at x iff for e being Real st 0 < e holds
ex H being Subset of S st
( H is open & x in H & ( for y being Point of S st y in H holds
dist ((In ((f . x),T)),(In ((f . y),T))) < e ) ) )