let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y
for x being Point of X holds
( f is_continuous_at x iff for G being a_neighborhood of f . x holds f " G is a_neighborhood of x )
let f be Function of X,Y; :: thesis: for x being Point of X holds
( f is_continuous_at x iff for G being a_neighborhood of f . x holds f " G is a_neighborhood of x )
let x be Point of X; :: thesis: ( f is_continuous_at x iff for G being a_neighborhood of f . x holds f " G is a_neighborhood of x )
thus ( f is_continuous_at x implies for G being a_neighborhood of f . x holds f " G is a_neighborhood of x ) :: thesis: ( ( for G being a_neighborhood of f . x holds f " G is a_neighborhood of x ) implies f is_continuous_at x )

proof

assume A1: f is_continuous_at x ; :: thesis: for G being a_neighborhood of f . x holds f " G is a_neighborhood of x
let G be a_neighborhood of f . x; :: thesis: f " G is a_neighborhood of x
consider H being a_neighborhood of x such that
A2: f .: H c= G by A1;
ex V being Subset of X st
( V is open & V c= f " G & x in V )

proof

consider V being Subset of X such that
A3: ( V is open & V c= H & x in V ) by CONNSP_2:6;
take V ; :: thesis: ( V is open & V c= f " G & x in V )
H c= f " G by A2, FUNCT_2:95;
hence ( V is open & V c= f " G & x in V ) by A3, XBOOLE_1:1; :: thesis: verum

end;

hence f " G is a_neighborhood of x by CONNSP_2:6; :: thesis: verum

end;

assume A4: for G being a_neighborhood of f . x holds f " G is a_neighborhood of x ; :: thesis: f is_continuous_at x
let G be a_neighborhood of f . x; :: according to TMAP_1:def 2 :: thesis: ex H being a_neighborhood of x st f .: H c= G
reconsider H = f " G as a_neighborhood of x by A4;
take H ; :: thesis: f .: H c= G
thus f .: H c= G by FUNCT_1:75; :: thesis: verum