set D = bool the carrier of T;

( S is open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense ) ; :: thesis: T is Baire

deffunc H_{1}( Element of bool the carrier of T) -> Element of bool the carrier of T = Int $1;

let F be Subset-Family of T; :: according to YELLOW_8:def 2 :: thesis: ( not F is countable or ex b_{1} being Element of bool the carrier of T st

( b_{1} in F & not b_{1} is everywhere_dense ) or ex b_{1} being Element of bool the carrier of T st

( b_{1} = Intersect F & b_{1} is dense ) )

assume that

A5: F is countable and

A6: for S being Subset of T st S in F holds

S is everywhere_dense ; :: thesis: ex b_{1} being Element of bool the carrier of T st

( b_{1} = Intersect F & b_{1} is dense )

set F1 = { (Int A) where A is Subset of T : A in F } ;

consider f being Function of (bool the carrier of T),(bool the carrier of T) such that

A7: for x being Element of bool the carrier of T holds f . x = H_{1}(x)
from FUNCT_2:sch 4();

{ (Int A) where A is Subset of T : A in F } c= f .: F

then A9: { (Int A) where A is Subset of T : A in F } is countable by A5, Th1;

reconsider J = Intersect F as Subset of T ;

A10: { (Int A) where A is Subset of T : A in F } c= bool the carrier of T

thus J = Intersect F ; :: thesis: J is dense

reconsider F1 = { (Int A) where A is Subset of T : A in F } as Subset-Family of T by A10;

for X being set st X in F holds

Intersect F1 c= X

( I = Intersect F1 & I is dense ) by A4, A9;

hence J is dense by A13, TOPS_1:44; :: thesis: verum

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 open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense ) ) implies T is Baire )

assume A4:
for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds ( S is open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense ) ) 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 open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense )

thus for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds

( S is open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense ) :: thesis: verum

end;( S is open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense )

thus for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds

( S is open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense ) :: thesis: verum

proof

let F be Subset-Family of T; :: thesis: ( F is countable & ( for S being Subset of T st S in F holds

( S is open & S is dense ) ) implies ex I being Subset of T st

( I = Intersect F & I is dense ) )

assume that

A2: F is countable and

A3: for S being Subset of T st S in F holds

( S is open & S is dense ) ; :: thesis: ex I being Subset of T st

( I = Intersect F & I is dense )

for S being Subset of T st S in F holds

S is everywhere_dense

( I = Intersect F & I is dense ) by A1, A2; :: thesis: verum

end;( S is open & S is dense ) ) implies ex I being Subset of T st

( I = Intersect F & I is dense ) )

assume that

A2: F is countable and

A3: for S being Subset of T st S in F holds

( S is open & S is dense ) ; :: thesis: ex I being Subset of T st

( I = Intersect F & I is dense )

for S being Subset of T st S in F holds

S is everywhere_dense

proof

hence
ex I being Subset of T st
let S be Subset of T; :: thesis: ( S in F implies S is everywhere_dense )

assume S in F ; :: thesis: S is everywhere_dense

then ( S is open & S is dense ) by A3;

hence S is everywhere_dense by TOPS_3:36; :: thesis: verum

end;assume S in F ; :: thesis: S is everywhere_dense

then ( S is open & S is dense ) by A3;

hence S is everywhere_dense by TOPS_3:36; :: thesis: verum

( I = Intersect F & I is dense ) by A1, A2; :: thesis: verum

( S is open & S is dense ) ) holds

ex I being Subset of T st

( I = Intersect F & I is dense ) ; :: thesis: T is Baire

deffunc H

let F be Subset-Family of T; :: according to YELLOW_8:def 2 :: thesis: ( not F is countable or ex b

( b

( b

assume that

A5: F is countable and

A6: for S being Subset of T st S in F holds

S is everywhere_dense ; :: thesis: ex b

( b

set F1 = { (Int A) where A is Subset of T : A in F } ;

consider f being Function of (bool the carrier of T),(bool the carrier of T) such that

A7: for x being Element of bool the carrier of T holds f . x = H

{ (Int A) where A is Subset of T : A in F } c= f .: F

proof

then
card { (Int A) where A is Subset of T : A in F } c= card F
by CARD_1:66;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (Int A) where A is Subset of T : A in F } or q in f .: F )

assume q in { (Int A) where A is Subset of T : A in F } ; :: thesis: q in f .: F

then consider A being Subset of T such that

A8: ( q = Int A & A in F ) ;

( dom f = bool the carrier of T & f . A = Int A ) by A7, FUNCT_2:def 1;

hence q in f .: F by A8, FUNCT_1:def 6; :: thesis: verum

end;assume q in { (Int A) where A is Subset of T : A in F } ; :: thesis: q in f .: F

then consider A being Subset of T such that

A8: ( q = Int A & A in F ) ;

( dom f = bool the carrier of T & f . A = Int A ) by A7, FUNCT_2:def 1;

hence q in f .: F by A8, FUNCT_1:def 6; :: thesis: verum

then A9: { (Int A) where A is Subset of T : A in F } is countable by A5, Th1;

reconsider J = Intersect F as Subset of T ;

A10: { (Int A) where A is Subset of T : A in F } c= bool the carrier of T

proof

take
J
; :: thesis: ( J = Intersect F & J is dense )
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { (Int A) where A is Subset of T : A in F } or q in bool the carrier of T )

assume q in { (Int A) where A is Subset of T : A in F } ; :: thesis: q in bool the carrier of T

then ex A being Subset of T st

( q = Int A & A in F ) ;

hence q in bool the carrier of T ; :: thesis: verum

end;assume q in { (Int A) where A is Subset of T : A in F } ; :: thesis: q in bool the carrier of T

then ex A being Subset of T st

( q = Int A & A in F ) ;

hence q in bool the carrier of T ; :: thesis: verum

thus J = Intersect F ; :: thesis: J is dense

reconsider F1 = { (Int A) where A is Subset of T : A in F } as Subset-Family of T by A10;

for X being set st X in F holds

Intersect F1 c= X

proof

then A13:
Intersect F1 c= Intersect F
by MSSUBFAM:4;
let X be set ; :: thesis: ( X in F implies Intersect F1 c= X )

assume A11: X in F ; :: thesis: Intersect F1 c= X

reconsider X1 = X as Subset of T by A11;

A12: Int X1 in F1 by A11;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Intersect F1 or q in X )

assume q in Intersect F1 ; :: thesis: q in X

then ( Int X1 c= X1 & q in Int X1 ) by A12, SETFAM_1:43, TOPS_1:16;

hence q in X ; :: thesis: verum

end;assume A11: X in F ; :: thesis: Intersect F1 c= X

reconsider X1 = X as Subset of T by A11;

A12: Int X1 in F1 by A11;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in Intersect F1 or q in X )

assume q in Intersect F1 ; :: thesis: q in X

then ( Int X1 c= X1 & q in Int X1 ) by A12, SETFAM_1:43, TOPS_1:16;

hence q in X ; :: thesis: verum

now :: thesis: for S being Subset of T st S in F1 holds

( S is open & S is dense )

then
ex I being Subset of T st ( S is open & S is dense )

let S be Subset of T; :: thesis: ( S in F1 implies ( S is open & S is dense ) )

assume S in F1 ; :: thesis: ( S is open & S is dense )

then consider A being Subset of T such that

A14: S = Int A and

A15: A in F ;

A is everywhere_dense by A6, A15;

hence ( S is open & S is dense ) by A14, TOPS_3:35; :: thesis: verum

end;assume S in F1 ; :: thesis: ( S is open & S is dense )

then consider A being Subset of T such that

A14: S = Int A and

A15: A in F ;

A is everywhere_dense by A6, A15;

hence ( S is open & S is dense ) by A14, TOPS_3:35; :: thesis: verum

( I = Intersect F1 & I is dense ) by A4, A9;

hence J is dense by A13, TOPS_1:44; :: thesis: verum