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: 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 7;
then S ` is nowhere_dense by A3;
hence S is everywhere_dense by TOPS_3:39; :: thesis: verum

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: verum

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: T is Baire
let F be Subset-Family of T; :: according to YELLOW_8:def 2 :: 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
A6: F is countable and
A7: 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 I = Intersect F as Subset of T ;
take I ; :: thesis: ( I = Intersect F & I is dense )
thus I = Intersect F ; :: thesis: I is dense
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

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 7;
then S ` is everywhere_dense by A7;
hence S is nowhere_dense by TOPS_3:40; :: thesis: verum

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: verum