let X be non empty TopSpace; :: thesis: 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; :: thesis: 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:]; :: thesis: { 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

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in { x where x is Point of X : [:([#] Y),{x}:] c= G } or q in the carrier of X )
assume q in { x where x is Point of X : [:([#] Y),{x}:] c= G } ; :: thesis: q in the carrier of X
then consider x' being Point of X such that
A1: ( q = x' & [:([#] Y),{x'}:] c= G ) ;
thus q in the carrier of X by A1; :: thesis: verum

end;

then reconsider Q = { x where x is Point of X : [:([#] Y),{x}:] c= G } as Subset of X ;
defpred S₁[ 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
A2: for x being set holds
( x in RR iff ( x in bool Q & S₁[x] ) ) from XBOOLE_0:sch 1();
RR c= bool Q

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in RR or x in bool Q )
assume x in RR ; :: thesis: x in bool Q
hence x in bool Q by A2; :: thesis: verum

end;

then reconsider RR = RR as Subset-Family of Q ;
A3: union RR = Q

proof

thus union RR c= Q ; :: according to XBOOLE_0:def 10 :: thesis: Q c= union RR
thus Q c= union RR :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in Q or a in union RR )
assume a in Q ; :: thesis: a in union RR
then consider x' being Point of X such that
A4: ( a = x' & [:([#] Y),{x'}:] c= G ) ;
consider R being open Subset of X such that
A5: ( a in R & R c= Q ) by A4, Th13;
R in RR by A2, A5;
hence a in union RR by A5, TARSKI:def 4; :: thesis: verum

end;

end;

bool Q c= bool the carrier of X by ZFMISC_1:79;
then reconsider RR = RR as Subset-Family of X by XBOOLE_1:1;
RR c= the topology of X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in RR or x in the topology of X )
assume x in RR ; :: thesis: x in the topology of X
then consider y being set such that
A6: ( y in Q & ex S being Subset of X st
( S = x & S is open & y in S & S c= Q ) ) by A2;
consider S being Subset of X such that
A7: ( S = x & S is open & y in S & S c= Q ) by A6;
thus x in the topology of X by A7, PRE_TOPC:def 5; :: thesis: verum

end;

hence { x where x is Point of X : [:([#] Y),{x}:] c= G } in the topology of X by A3, PRE_TOPC:def 1; :: thesis: verum