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 } ) )
set y = the Point of Y;
A1: ( the carrier of [:Y,X:] = [: the carrier of Y, the carrier of X:] & [ the Point of Y,x] in [: the carrier of Y,{x}:] ) by BORSUK_1:def 2, ZFMISC_1:106;
assume A2: [:([#] 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 [:([#] Y),{x}:] c= the carrier of [:Y,X:] by XBOOLE_1:1;
then reconsider x9 = x as Point of X by A1, ZFMISC_1:87;
Int G = G by TOPS_1:23;
then ( [#] Y is compact & G is a_neighborhood of [:([#] Y),{x9}:] ) by A2, COMPTS_1:1, CONNSP_2:def 2;
then consider W being a_neighborhood of [#] Y, V being a_neighborhood of x9 such that
A3: [:W,V:] c= G by BORSUK_1:25;
take R = Int V; :: thesis: ( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } )
( Int W c= W & [#] Y c= Int W ) by CONNSP_2:def 2, TOPS_1:16;
then A4: [#] Y c= W ;
A5: Int V c= V by TOPS_1:16;
R c= { z where z is Point of X : [:([#] Y),{z}:] c= G }

proof

let r be object ; :: 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 A6: r in R ; :: thesis: r in { z where z is Point of X : [:([#] Y),{z}:] c= G }
then reconsider r9 = r as Point of X ;
{r} c= V by A5, A6, ZFMISC_1:31;
then [:([#] Y),{r9}:] c= [:W,V:] by A4, ZFMISC_1:96;
then [:([#] Y),{r9}:] c= G by A3;
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