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, YELLOW_8:def 3; :: 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
let F be Subset-Family of T; :: according to YELLOW_8:def 3 :: 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 } ;
set D = bool the carrier of T;
deffunc H₁( Element of bool the carrier of T) -> Element of bool the carrier of T = Int $1;
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 set ; :: 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 ) ;
A9: dom f = bool the carrier of T by FUNCT_2:def 1;
f . A = Int A by A7;
hence q in f .: F by A8, A9, FUNCT_1:def 12; :: thesis: verum

end;

then card { (Int A) where A is Subset of T : A in F } c= card F by CARD_2:2;
then A10: { (Int A) where A is Subset of T : A in F } is countable by A5, Th2;
{ (Int A) where A is Subset of T : A in F } c= bool the carrier of T

proof

let q be set ; :: 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 consider A being Subset of T such that
A11: q = Int A and
A in F ;
thus q in bool the carrier of T by A11; :: thesis: verum

end;

then reconsider F1 = { (Int A) where A is Subset of T : A in F } as Subset-Family of T ;

now

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
A12: S = Int A and
A13: A in F ;
A is everywhere_dense by A6, A13;
hence ( S is open & S is dense ) by A12, TOPS_1:51, TOPS_3:35; :: thesis: verum

end;

then consider I being Subset of T such that
A14: ( I = Intersect F1 & I is dense ) by A4, A10;
reconsider J = Intersect F as Subset of T ;
take J ; :: thesis: ( J = Intersect F & J is dense )
thus J = Intersect F ; :: thesis: J is dense
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 A15: X in F ; :: thesis: Intersect F1 c= X
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in Intersect F1 or q in X )
assume A16: q in Intersect F1 ; :: thesis: q in X
reconsider X1 = X as Subset of T by A15;
A17: Int X1 c= X1 by TOPS_1:44;
Int X1 in F1 by A15;
then q in Int X1 by A16, SETFAM_1:58;
hence q in X by A17; :: thesis: verum

end;

then Intersect F1 c= Intersect F by MSSUBFAM:4;
hence J is dense by A14, TOPS_1:79; :: thesis: verum