set D = bool the carrier of T;

assume A1: T is Baire ; :: thesis:
thus for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
( S is open & S is dense ) ) holds
ex I being Subset of T st
( I = Intersect F & I is dense ) :: thesis:

end;

end;

assume A4: for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
( S is open & S is dense ) ) holds
ex I being Subset of T st
( I = Intersect F & I is dense ) ; :: thesis:
deffunc H₁( Element of bool the carrier of T) -> Element of bool the carrier of T = Int $1;
let F be Subset-Family of T; :: according to YELLOW_8:def 2 :: thesis:
assume that
A5: F is countable and
A6: for S being Subset of T st S in F holds
S is everywhere_dense ; :: thesis:
set F1 = { (Int A) where A is Subset of T : A in F } ;
consider f being Function of (bool the carrier of T),(bool the carrier of T) such that
A7: for x being Element of bool the carrier of T holds f . x = H₁(x) from FUNCT_2:sch 4();
{ (Int A) where A is Subset of T : A in F } c= f .: F

let q be object ; :: according to TARSKI:def 3 :: thesis:
assume q in { (Int A) where A is Subset of T : A in F } ; :: thesis:
then consider A being Subset of T such that
A8: ( q = Int A & A in F ) ;
( dom f = bool the carrier of T & f . A = Int A ) by A7, FUNCT_2:def 1;
hence q in f .: F by A8, FUNCT_1:def 6; :: thesis:

end;

then card { (Int A) where A is Subset of T : A in F } c= card F by CARD_1:66;
then A9: { (Int A) where A is Subset of T : A in F } is countable by A5, Th1;
reconsider J = Intersect F as Subset of T ;
A10: { (Int A) where A is Subset of T : A in F } c= bool the carrier of T

let q be object ; :: according to TARSKI:def 3 :: thesis:
assume q in { (Int A) where A is Subset of T : A in F } ; :: thesis:
then ex A being Subset of T st
( q = Int A & A in F ) ;
hence q in bool the carrier of T ; :: thesis:

end;

take J ; :: thesis:
thus J = Intersect F ; :: thesis:
reconsider F1 = { (Int A) where A is Subset of T : A in F } as Subset-Family of T by A10;
for X being set st X in F holds
Intersect F1 c= X

let X be set ; :: thesis:
assume A11: X in F ; :: thesis:
reconsider X1 = X as Subset of T by A11;
A12: Int X1 in F1 by A11;
let q be object ; :: according to TARSKI:def 3 :: thesis:
assume q in Intersect F1 ; :: thesis:
then ( Int X1 c= X1 & q in Int X1 ) by A12, SETFAM_1:43, TOPS_1:16;
hence q in X ; :: thesis:

end;

end;