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 )

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

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 A6:
for G being Subset of Y st G is open & f . x in G holds
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;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

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