theorem Th3: :: CC0SP2:3

for X being non empty TopSpace
for f being Function of the carrier of X,COMPLEX holds
( f is continuous iff for x being Point of X
for V being Subset of COMPLEX st f . x in V & V is open holds
ex W being Subset of X st
( x in W & W is open & f .: W c= V ) )