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 Subset of Y st G is open & f . x in G holds
ex H being Subset of X st
( H is open & x in H & f .: H c= G ) )
let f be Function of X,Y; :: thesis: for x being Point of X holds
( f is_continuous_at x iff for G being Subset of Y st G is open & f . x in G holds
ex H being Subset of X st
( H is open & x in H & f .: H c= G ) )
let x be Point of X; :: thesis: ( f is_continuous_at x iff for G being Subset of Y st G is open & f . x in G holds
ex H being Subset of X st
( H is open & x in H & f .: H c= G ) )
thus ( f is_continuous_at x implies for G being Subset of Y st G is open & f . x in G holds
ex H being Subset of X st
( H is open & x in H & f .: H c= G ) ) :: thesis: ( ( for G being Subset of Y st G is open & f . x in G holds
ex H being Subset of X st
( H is open & x in H & f .: H c= G ) ) implies f is_continuous_at x )

proof

assume A1: f is_continuous_at x ; :: thesis: for G being Subset of Y st G is open & f . x in G holds
ex H being Subset of X st
( H is open & x in H & f .: H c= G )
let G be Subset of Y; :: thesis: ( G is open & f . x in G implies ex H being Subset of X st
( H is open & x in H & f .: H c= G ) )
assume ( G is open & f . x in G ) ; :: thesis: ex H being Subset of X st
( H is open & x in H & f .: H c= G )
then reconsider G0 = G as a_neighborhood of f . x by CONNSP_2:3;
consider H0 being a_neighborhood of x such that
A2: f .: H0 c= G0 by A1;
consider H being Subset of X such that
A3: H is open and
A4: H c= H0 and
A5: x in H by CONNSP_2:6;
take H ; :: thesis: ( H is open & x in H & f .: H c= G )
f .: H c= f .: H0 by A4, RELAT_1:123;
hence ( H is open & x in H & f .: H c= G ) by A2, A3, A5, XBOOLE_1:1; :: thesis: verum

end;

assume A6: for G being Subset of Y st G is open & f . x in G holds
ex H being Subset of X st
( H is open & x in H & f .: H c= G ) ; :: thesis: f is_continuous_at x
let G0 be a_neighborhood of f . x; :: according to TMAP_1:def 2 :: thesis: ex H being a_neighborhood of x st f .: H c= G0
consider G being Subset of Y such that
A7: G is open and
A8: G c= G0 and
A9: f . x in G by CONNSP_2:6;
consider H being Subset of X such that
A10: ( H is open & x in H ) and
A11: f .: H c= G by A6, A7, A9;
reconsider H0 = H as a_neighborhood of x by A10, CONNSP_2:3;
take H0 ; :: thesis: f .: H0 c= G0
thus f .: H0 c= G0 by A8, A11, XBOOLE_1:1; :: thesis: verum