let X be non empty TopSpace; :: thesis: for Y being non empty compact TopSpace
for G being open Subset of [:Y,X:]
for x being set st [:([#] Y),{x}:] c= G holds
ex R being open Subset of X st
( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } )
let Y be non empty compact TopSpace; :: thesis: for G being open Subset of [:Y,X:]
for x being set st [:([#] Y),{x}:] c= G holds
ex R being open Subset of X st
( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } )
let G be open Subset of [:Y,X:]; :: thesis: for x being set st [:([#] Y),{x}:] c= G holds
ex R being open Subset of X st
( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } )
let x be set ; :: thesis: ( [:([#] Y),{x}:] c= G implies ex R being open Subset of X st
( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } ) )
assume A1: [:([#] Y),{x}:] c= G ; :: thesis: ex R being open Subset of X st
( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } )
then A2: [:([#] Y),{x}:] c= the carrier of [:Y,X:] by XBOOLE_1:1;
A3: the carrier of [:Y,X:] = [:the carrier of Y,the carrier of X:] by BORSUK_1:def 5;
consider y being Point of Y;
[y,x] in [:the carrier of Y,{x}:] by ZFMISC_1:129;
then reconsider x' = x as Point of X by A2, A3, ZFMISC_1:106;
A4: [#] Y is compact by COMPTS_1:10;
Int G = G by TOPS_1:55;
then G is a_neighborhood of [:([#] Y),{x'}:] by A1, CONNSP_2:def 2;
then consider W being a_neighborhood of [#] Y, V being a_neighborhood of x' such that
A5: [:W,V:] c= G by A4, BORSUK_1:67;
take R = Int V; :: thesis: ( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } )
A6: ( Int W c= W & Int V c= V ) by TOPS_1:44;
[#] Y c= Int W by CONNSP_2:def 2;
then A7: [#] Y c= W by A6, XBOOLE_1:1;
R c= { z where z is Point of X : [:([#] Y),{z}:] c= G }

proof

let r be set ; :: according to TARSKI:def 3 :: thesis: ( not r in R or r in { z where z is Point of X : [:([#] Y),{z}:] c= G } )
assume A8: r in R ; :: thesis: r in { z where z is Point of X : [:([#] Y),{z}:] c= G }
then reconsider r' = r as Point of X ;
{r} c= V by A6, A8, ZFMISC_1:37;
then [:([#] Y),{r'}:] c= [:W,V:] by A7, ZFMISC_1:119;
then [:([#] Y),{r'}:] c= G by A5, XBOOLE_1:1;
hence r in { z where z is Point of X : [:([#] Y),{z}:] c= G } ; :: thesis: verum

end;

hence ( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } ) by CONNSP_2:def 1; :: thesis: verum