let T be non empty TopSpace; :: thesis:

hereby :: thesis:

assume A1: T is Baire ; :: thesis:
let F be Subset-Family of T; :: thesis:
assume that
A2: F is countable and
A3: for S being Subset of T st S in F holds
S is nowhere_dense ; :: thesis:
reconsider G = COMPLEMENT F as Subset-Family of T ;
A4: for S being Subset of T st S in G holds
S is everywhere_dense

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

end;

G is countable by A2, Th3, Th4;
then ex I being Subset of T st
( I = Intersect G & I is dense ) by A1, A4;
then (union F) ` is dense by Th6;
hence union F is boundary by TOPS_1:def 4; :: thesis:

end;

assume A5: 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:
let F be Subset-Family of T; :: according to YELLOW_8:def 2 :: thesis:
assume that
A6: F is countable and
A7: for S being Subset of T st S in F holds
S is everywhere_dense ; :: thesis:
reconsider I = Intersect F as Subset of T ;
take I ; :: thesis:
thus I = Intersect F ; :: thesis:
reconsider G = COMPLEMENT F as Subset-Family of T ;
A8: for S being Subset of T st S in G holds
S is nowhere_dense

let S be Subset of T; :: thesis:
assume S in G ; :: thesis:
then S ` in F by SETFAM_1:def 7;
then S ` is everywhere_dense by A7;
hence S is nowhere_dense by TOPS_3:40; :: thesis:

end;

G is countable by A6, Th3, Th4;
then union G is boundary by A5, A8;
then (Intersect F) ` is boundary by Th7;
hence I is dense by TOPS_3:18; :: thesis: