let X be non empty TopSpace; 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; 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:]; 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 ; ( [:([#] 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
; 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; ( 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 }
hence
( x in R & R c= { y where y is Point of X : [:([#] Y),{y}:] c= G } )
by CONNSP_2:def 1; verum