thus ( f is continuous implies for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N ) :: thesis: ( ( for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N ) implies f is continuous )
proof
assume A1: f is continuous ; :: thesis: for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N
let p be Point of T; :: thesis: for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N
let N be Neighbourhood of f . p; :: thesis: ex V being a_neighborhood of p st f .: V c= N
A2: f " (N `) = (f " N) ` by FUNCT_2:100;
N ` is closed by RCOMP_1:def 5;
then f " (N `) is closed by A1;
then A3: f " N is open by A2, TOPS_1:4;
f . p in N by RCOMP_1:16;
then p in f " N by FUNCT_2:38;
then reconsider V = f " N as a_neighborhood of p by A3, CONNSP_2:3;
take V ; :: thesis: f .: V c= N
thus f .: V c= N by FUNCT_1:75; :: thesis: verum
end;
assume A4: for p being Point of T
for N being Neighbourhood of f . p ex V being a_neighborhood of p st f .: V c= N ; :: thesis: f is continuous
let Y be Subset of REAL; :: according to PSCOMP_1:def 3 :: thesis: ( not Y is closed or f " Y is closed )
assume Y is closed ; :: thesis: f " Y is closed
then (Y `) ` is closed ;
then A5: Y ` is open by RCOMP_1:def 5;
for p being Point of T st p in (f " Y) ` holds
ex A being Subset of T st
( A is a_neighborhood of p & A c= (f " Y) ` )
proof
let p be Point of T; :: thesis: ( p in (f " Y) ` implies ex A being Subset of T st
( A is a_neighborhood of p & A c= (f " Y) ` ) )
assume p in (f " Y) ` ; :: thesis: ex A being Subset of T st
( A is a_neighborhood of p & A c= (f " Y) ` )
then p in f " (Y `) by FUNCT_2:100;
then f . p in Y ` by FUNCT_2:38;
then consider N being Neighbourhood of f . p such that
A6: N c= Y ` by A5, RCOMP_1:18;
consider V being a_neighborhood of p such that
A7: f .: V c= N by A4;
take V ; :: thesis: ( V is a_neighborhood of p & V c= (f " Y) ` )
thus V is a_neighborhood of p ; :: thesis: V c= (f " Y) `
f .: V c= Y ` by A6, A7;
then A8: f " (f .: V) c= f " (Y `) by RELAT_1:143;
V c= f " (f .: V) by FUNCT_2:42;
then V c= f " (Y `) by A8;
hence V 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