let T be non empty TopSpace; :: thesis: ( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is nowhere_dense ) holds
union F is boundary )

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 nowhere_dense ) holds
union F is boundary ) 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 nowhere_dense ) holds
union F is boundary
let F be Subset-Family of T; :: thesis: ( F is countable & ( for S being Subset of T st S in F holds
S is nowhere_dense ) implies union F is boundary )
assume that
A2: F is countable and
A3: for S being Subset of T st S in F holds
S is nowhere_dense ; :: thesis: union F is boundary
reconsider G = COMPLEMENT F as Subset-Family of T ;
A4: G is countable by A2, Th4, Th5;
for S being Subset of T st S in G holds
S is everywhere_dense

proof

let S be Subset of T; :: thesis: ( S in G implies S is everywhere_dense )
assume S in G ; :: thesis: S is everywhere_dense
then S ` in F by SETFAM_1:def 8;
then S ` is nowhere_dense by A3;
hence S is everywhere_dense by TOPS_3:39; :: thesis: verum

end;

then consider I being Subset of T such that
A5: ( I = Intersect G & I is dense ) by A1, A4, Def3;
(union F) ` is dense by A5, Th15;
hence union F is boundary by TOPS_1:def 4; :: thesis: verum

end;

assume A6: for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is nowhere_dense ) holds
union F is boundary ; :: thesis: T is Baire
let F be Subset-Family of T; :: according to YELLOW_8:def 3 :: thesis: ( F is countable & ( for S being Subset of T st S in F holds
S is everywhere_dense ) implies ex I being Subset of T st
( I = Intersect F & I is dense ) )
assume that
A7: F is countable and
A8: for S being Subset of T st S in F holds
S is everywhere_dense ; :: thesis: ex I being Subset of T st
( I = Intersect F & I is dense )
reconsider G = COMPLEMENT F as Subset-Family of T ;
A9: G is countable by A7, Th4, Th5;
reconsider I = Intersect F as Subset of T ;
take I ; :: thesis: ( I = Intersect F & I is dense )
thus I = Intersect F ; :: thesis: I is dense
for S being Subset of T st S in G holds
S is nowhere_dense

proof

let S be Subset of T; :: thesis: ( S in G implies S is nowhere_dense )
assume S in G ; :: thesis: S is nowhere_dense
then S ` in F by SETFAM_1:def 8;
then S ` is everywhere_dense by A8;
hence S is nowhere_dense by TOPS_3:40; :: thesis: verum

end;

then union G is boundary by A6, A9;
then (Intersect F) ` is boundary by Th16;
hence I is dense by TOPS_3:18; :: thesis: verum