for X being non empty TopSpace
for f being RealMap of X holds
( f is continuous iff for x being Point of X
for V being Subset of REAL 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 ) )