let X be non empty TopSpace; :: thesis: 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 ) )
let f be RealMap of X; :: thesis: ( 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 ) )

hereby :: thesis: ( ( 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 ) ) implies f is continuous )

assume A1: f is continuous ; :: thesis: 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 )

now :: thesis: for x being Point of X
for V being Subset of REAL st f . x in V & V is open holds
ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V )

let x be Point of X; :: thesis: for V being Subset of REAL st f . x in V & V is open holds
ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V )
let V be Subset of REAL; :: thesis: ( f . x in V & V is open implies ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V ) )
set r = f . x;
assume ( f . x in V & V is open ) ; :: thesis: ex W being Element of bool the carrier of X st
( x in W & W is open & f .: W c= V )
then consider r0 being Real such that
A2: ( 0 < r0 & ].((f . x) - r0),((f . x) + r0).[ c= V ) by RCOMP_1:19;
set S = ].((f . x) - r0),((f . x) + r0).[;
take W = f " ].((f . x) - r0),((f . x) + r0).[; :: thesis: ( x in W & W is open & f .: W c= V )
|.((f . x) - (f . x)).| < r0 by A2, COMPLEX1:44;
then f . x in ].((f . x) - r0),((f . x) + r0).[ by RCOMP_1:1;
hence x in W by FUNCT_2:38; :: thesis: ( W is open & f .: W c= V )
thus W is open by A1, PSCOMP_1:8; :: thesis: f .: W c= V
f .: (f " ].((f . x) - r0),((f . x) + r0).[) c= ].((f . x) - r0),((f . x) + r0).[ by FUNCT_1:75;
hence f .: W c= V by A2; :: thesis: verum

end;

hence 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 ) ; :: thesis: verum

end;

assume A3: 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 ) ; :: thesis: f is continuous

now :: thesis: for Y being Subset of REAL st Y is closed holds
f " Y is closed

let Y be Subset of REAL; :: thesis: ( Y is closed implies f " Y is closed )
assume Y is closed ; :: thesis: f " Y is closed
then (Y `) ` is closed ;
then A4: Y ` is open ;
for x being Point of X st x in (f " Y) ` holds
ex W being Subset of X st
( W is a_neighborhood of x & W c= (f " Y) ` )

proof

let x be Point of X; :: thesis: ( x in (f " Y) ` implies ex W being Subset of X st
( W is a_neighborhood of x & W c= (f " Y) ` ) )
assume x in (f " Y) ` ; :: thesis: ex W being Subset of X st
( W is a_neighborhood of x & W c= (f " Y) ` )
then x in f " (Y `) by FUNCT_2:100;
then f . x in Y ` by FUNCT_2:38;
then consider V being Subset of REAL such that
A5: ( f . x in V & V is open & V c= Y ` ) by A4;
consider W being Subset of X such that
A6: ( x in W & W is open & f .: W c= V ) by A3, A5;
take W ; :: thesis: ( W is a_neighborhood of x & W c= (f " Y) ` )
thus W is a_neighborhood of x by A6, CONNSP_2:3; :: thesis: W c= (f " Y) `
f .: W c= Y ` by A5, A6;
then A7: f " (f .: W) c= f " (Y `) by RELAT_1:143;
W c= f " (f .: W) by FUNCT_2:42;
then W c= f " (Y `) by A7;
hence W c= (f " Y) ` by FUNCT_2:100; :: thesis: verum

end;

then (f " Y) ` is open by CONNSP_2:7;
then ((f " Y) `) ` is closed by TOPS_1:4;
hence f " Y is closed ; :: thesis: verum

end;

hence f is continuous ; :: thesis: verum