let X be non empty TopSpace; for Y being non empty compact TopSpace
for G being open Subset of [:Y,X:] holds { x where x is Point of X : [:([#] Y),{x}:] c= G } in the topology of X
let Y be non empty compact TopSpace; for G being open Subset of [:Y,X:] holds { x where x is Point of X : [:([#] Y),{x}:] c= G } in the topology of X
let G be open Subset of [:Y,X:]; { x where x is Point of X : [:([#] Y),{x}:] c= G } in the topology of X
set Q = { x where x is Point of X : [:([#] Y),{x}:] c= G } ;
{ x where x is Point of X : [:([#] Y),{x}:] c= G } c= the carrier of X
then reconsider Q = { x where x is Point of X : [:([#] Y),{x}:] c= G } as Subset of X ;
defpred S1[ set ] means ex y being set st
( y in Q & ex S being Subset of X st
( S = $1 & S is open & y in S & S c= Q ) );
consider RR being set such that
A1:
for x being set holds
( x in RR iff ( x in bool Q & S1[x] ) )
from XFAMILY:sch 1();
RR c= bool Q
by A1;
then reconsider RR = RR as Subset-Family of Q ;
Q c= union RR
then A4:
union RR = Q
;
bool Q c= bool the carrier of X
by ZFMISC_1:67;
then reconsider RR = RR as Subset-Family of X by XBOOLE_1:1;
RR c= the topology of X
hence
{ x where x is Point of X : [:([#] Y),{x}:] c= G } in the topology of X
by A4, PRE_TOPC:def 1; verum