theorem Th3: :: ASCOLI:3

for S being non empty TopSpace
for T being NormedLinearTopSpace
for f being Function of S,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
||.((f . x) - (f . y)).|| < e ) ) )