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:
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 H1( 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 b1 being Element of bool the carrier of T st
( b1 in F & not b1 is everywhere_dense ) or ex b1 being Element of bool the carrier of T st
( b1 = Intersect F & b1 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 b1 being Element of bool the carrier of T st
( b1 = Intersect F & b1 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 = H1(x) from { (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 ;
hence q in f .: F by ; :: 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 ;
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 ;
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 ;
hence ( S is open & S is dense ) by ; :: 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 ; :: thesis: verum