A1:
[#] Y <> {}
;

thus ( F is continuous implies for W being Point of X

for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ) :: thesis: ( ( for W being Point of X

for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ) implies F is continuous )

for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ; :: thesis: F is continuous

thus ( F is continuous implies for W being Point of X

for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ) :: thesis: ( ( for W being Point of X

for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ) implies F is continuous )

proof

assume A4:
for W being Point of X
assume A2:
F is continuous
; :: thesis: for W being Point of X

for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G

let W be Point of X; :: thesis: for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G

let G be a_neighborhood of F . W; :: thesis: ex H being a_neighborhood of W st F .: H c= G

F . W in Int G by CONNSP_2:def 1;

then A3: W in F " (Int G) by FUNCT_2:38;

F " (Int G) is open by A1, A2, TOPS_2:43;

then W in Int (F " (Int G)) by A3, TOPS_1:23;

then reconsider H = F " (Int G) as a_neighborhood of W by CONNSP_2:def 1;

take H ; :: thesis: F .: H c= G

H c= F " G by RELAT_1:143, TOPS_1:16;

hence F .: H c= G by EQREL_1:46; :: thesis: verum

end;for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G

let W be Point of X; :: thesis: for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G

let G be a_neighborhood of F . W; :: thesis: ex H being a_neighborhood of W st F .: H c= G

F . W in Int G by CONNSP_2:def 1;

then A3: W in F " (Int G) by FUNCT_2:38;

F " (Int G) is open by A1, A2, TOPS_2:43;

then W in Int (F " (Int G)) by A3, TOPS_1:23;

then reconsider H = F " (Int G) as a_neighborhood of W by CONNSP_2:def 1;

take H ; :: thesis: F .: H c= G

H c= F " G by RELAT_1:143, TOPS_1:16;

hence F .: H c= G by EQREL_1:46; :: thesis: verum

for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G ; :: thesis: F is continuous

now :: thesis: for P1 being Subset of Y st P1 is open holds

F " P1 is open

hence
F is continuous
by A1, TOPS_2:43; :: thesis: verumF " P1 is open

let P1 be Subset of Y; :: thesis: ( P1 is open implies F " P1 is open )

assume A5: P1 is open ; :: thesis: F " P1 is open

end;assume A5: P1 is open ; :: thesis: F " P1 is open

now :: thesis: for x being set holds

( ( x in F " P1 implies ex P being Subset of X st

( P is open & P c= F " P1 & x in P ) ) & ( ex P being Subset of X st

( P is open & P c= F " P1 & x in P ) implies x in F " P1 ) )

hence
F " P1 is open
by TOPS_1:25; :: thesis: verum( ( x in F " P1 implies ex P being Subset of X st

( P is open & P c= F " P1 & x in P ) ) & ( ex P being Subset of X st

( P is open & P c= F " P1 & x in P ) implies x in F " P1 ) )

let x be set ; :: thesis: ( ( x in F " P1 implies ex P being Subset of X st

( P is open & P c= F " P1 & x in P ) ) & ( ex P being Subset of X st

( P is open & P c= F " P1 & x in P ) implies x in F " P1 ) )

thus ( x in F " P1 implies ex P being Subset of X st

( P is open & P c= F " P1 & x in P ) ) :: thesis: ( ex P being Subset of X st

( P is open & P c= F " P1 & x in P ) implies x in F " P1 )

( P is open & P c= F " P1 & x in P ) implies x in F " P1 ) ; :: thesis: verum

end;( P is open & P c= F " P1 & x in P ) ) & ( ex P being Subset of X st

( P is open & P c= F " P1 & x in P ) implies x in F " P1 ) )

thus ( x in F " P1 implies ex P being Subset of X st

( P is open & P c= F " P1 & x in P ) ) :: thesis: ( ex P being Subset of X st

( P is open & P c= F " P1 & x in P ) implies x in F " P1 )

proof

thus
( ex P being Subset of X st
assume A6:
x in F " P1
; :: thesis: ex P being Subset of X st

( P is open & P c= F " P1 & x in P )

then reconsider W = x as Point of X ;

A7: Int P1 = P1 by A5, TOPS_1:23;

F . W in P1 by A6, FUNCT_2:38;

then P1 is a_neighborhood of F . W by A7, CONNSP_2:def 1;

then consider H being a_neighborhood of W such that

A8: F .: H c= P1 by A4;

take Int H ; :: thesis: ( Int H is open & Int H c= F " P1 & x in Int H )

thus Int H is open ; :: thesis: ( Int H c= F " P1 & x in Int H )

A9: Int H c= H by TOPS_1:16;

dom F = the carrier of X by FUNCT_2:def 1;

then A10: H c= F " (F .: H) by FUNCT_1:76;

F " (F .: H) c= F " P1 by A8, RELAT_1:143;

then H c= F " P1 by A10;

hence Int H c= F " P1 by A9; :: thesis: x in Int H

thus x in Int H by CONNSP_2:def 1; :: thesis: verum

end;( P is open & P c= F " P1 & x in P )

then reconsider W = x as Point of X ;

A7: Int P1 = P1 by A5, TOPS_1:23;

F . W in P1 by A6, FUNCT_2:38;

then P1 is a_neighborhood of F . W by A7, CONNSP_2:def 1;

then consider H being a_neighborhood of W such that

A8: F .: H c= P1 by A4;

take Int H ; :: thesis: ( Int H is open & Int H c= F " P1 & x in Int H )

thus Int H is open ; :: thesis: ( Int H c= F " P1 & x in Int H )

A9: Int H c= H by TOPS_1:16;

dom F = the carrier of X by FUNCT_2:def 1;

then A10: H c= F " (F .: H) by FUNCT_1:76;

F " (F .: H) c= F " P1 by A8, RELAT_1:143;

then H c= F " P1 by A10;

hence Int H c= F " P1 by A9; :: thesis: x in Int H

thus x in Int H by CONNSP_2:def 1; :: thesis: verum

( P is open & P c= F " P1 & x in P ) implies x in F " P1 ) ; :: thesis: verum