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 )

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

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

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

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

G is countable
by A2, Th3, Th4;
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;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

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

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

G is countable
by A6, Th3, Th4;
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;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

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