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