let X be non empty TopSpace; :: thesis: for Y being non empty compact TopSpace
for G being open Subset of holds { x where x is Point of : [:([#] Y),{x}:] c= G } in the topology of X
let Y be non empty compact TopSpace; :: thesis: for G being open Subset of holds { x where x is Point of : [:([#] Y),{x}:] c= G } in the topology of X
let G be open Subset of ; :: thesis: { x where x is Point of : [:([#] Y),{x}:] c= G } in the topology of X
set Q = { x where x is Point of : [:([#] Y),{x}:] c= G } ;
{ x where x is Point of : [:([#] 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 : [:([#] Y),{x}:] c= G } or q in the carrier of X )
assume q in { x where x is Point of : [:([#] Y),{x}:] c= G } ; :: thesis: q in the carrier of X
then ex x' being Point of st
( q = x' & [:([#] Y),{x'}:] c= G ) ;
hence q in the carrier of X ; :: thesis: verum

end;

then reconsider Q = { x where x is Point of : [:([#] Y),{x}:] c= G } as Subset of ;
defpred S₁[ set ] means ex y being set st
( y in Q & ex S being Subset of 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 & 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 A1; :: thesis: verum

end;

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

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 ex x' being Point of st
( a = x' & [:([#] Y),{x'}:] c= G ) ;
then consider R being open Subset of such that
A2: a in R and
A3: R c= Q by Th13;
R in RR by A1, A2, A3;
hence a in union RR by A2, TARSKI:def 4; :: thesis: verum

end;

then A4: union RR = Q by XBOOLE_0:def 10;
bool Q c= bool the carrier of X by ZFMISC_1:79;
then reconsider RR = RR as Subset-Family of 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 ex y being set st
( y in Q & ex S being Subset of st
( S = x & S is open & y in S & S c= Q ) ) by A1;
hence x in the topology of X by PRE_TOPC:def 5; :: thesis: verum

end;

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