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 )

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) ` )

then ((f " Y) `) ` is closed by TOPS_1:4;

hence f " Y is closed ; :: thesis: verum

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 A4:
for p being Point of T
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;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

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

then
(f " Y) ` is open
by CONNSP_2:7;
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;( 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

then ((f " Y) `) ` is closed by TOPS_1:4;

hence f " Y is closed ; :: thesis: verum