set D = bool the carrier of T;

hereby :: thesis: ( ( 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 ) ) implies T is Baire )

assume A1: T is Baire ; :: thesis: 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 )
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: verum

proof

let F be Subset-Family of T; :: thesis: ( F is countable & ( for S being Subset of T st S in F holds
( S is open & S is dense ) ) implies ex I being Subset of T st
( I = Intersect F & I is dense ) )
assume that
A2: F is countable and
A3: for S being Subset of T st S in F holds
( S is open & S is dense ) ; :: thesis: ex I being Subset of T st
( I = Intersect F & I is dense )
for S being Subset of T st S in F holds
S is everywhere_dense

proof

let S be Subset of T; :: thesis: ( S in F implies S is everywhere_dense )
assume S in F ; :: thesis: S is everywhere_dense
then ( S is open & S is dense ) by A3;
hence S is everywhere_dense by TOPS_3:36; :: thesis: verum

end;

hence ex I being Subset of T st
( I = Intersect F & I is dense ) by A1, A2; :: thesis: verum

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: T is Baire
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: ( not F is countable or ex b₁ being Element of bool the carrier of T st
( b₁ in F & not b₁ is everywhere_dense ) or ex b₁ being Element of bool the carrier of T st
( b₁ = Intersect F & b₁ is dense ) )
assume that
A5: F is countable and
A6: for S being Subset of T st S in F holds
S is everywhere_dense ; :: thesis: ex b₁ being Element of bool the carrier of T st
( b₁ = Intersect F & b₁ is dense )
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

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (Int A) where A is Subset of T : A in F } or q in f .: F )
assume q in { (Int A) where A is Subset of T : A in F } ; :: thesis: q in f .: F
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: verum

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

proof

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

end;

take J ; :: thesis: ( J = Intersect F & J is dense )
thus J = Intersect F ; :: thesis: J is dense
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

proof

let X be set ; :: thesis: ( X in F implies Intersect F1 c= X )
assume A11: X in F ; :: thesis: Intersect F1 c= X
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: ( not q in Intersect F1 or q in X )
assume q in Intersect F1 ; :: thesis: q in X
then ( Int X1 c= X1 & q in Int X1 ) by A12, SETFAM_1:43, TOPS_1:16;
hence q in X ; :: thesis: verum

end;

then A13: Intersect F1 c= Intersect F by MSSUBFAM:4;

now :: thesis: for S being Subset of T st S in F1 holds
( S is open & S is dense )

let S be Subset of T; :: thesis: ( S in F1 implies ( S is open & S is dense ) )
assume S in F1 ; :: thesis: ( S is open & S is dense )
then consider A being Subset of T such that
A14: S = Int A and
A15: A in F ;
A is everywhere_dense by A6, A15;
hence ( S is open & S is dense ) by A14, TOPS_3:35; :: thesis: verum

end;

then ex I being Subset of T st
( I = Intersect F1 & I is dense ) by A4, A9;
hence J is dense by A13, TOPS_1:44; :: thesis: verum