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 object ; :: 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 ex x9 being Point of X st
( q = x9 & [:([#] Y),{x9}:] c= G ) ;
hence q in the carrier of X ; :: 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
A1: for x being set holds
( x in RR iff ( x in bool Q & S₁[x] ) ) from XFAMILY:sch 1();
RR c= bool Q by A1;
then reconsider RR = RR as Subset-Family of Q ;
Q c= union RR

proof

let a be object ; :: 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 x9 being Point of X st
( a = x9 & [:([#] Y),{x9}:] c= G ) ;
then consider R being open Subset of X such that
A2: a in R and
A3: R c= Q by Th11;
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 ;
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

proof

let x be object ; :: 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 X 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 2; :: thesis: verum

end;

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