let T be non empty TopSpace; :: thesis: ( T is sober & T is locally-compact implies T is Baire )

assume A1: ( T is sober & T is locally-compact ) ; :: thesis: T is Baire

let F be Subset-Family of T; :: according to WAYBEL12:def 6 :: 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 )

A4: F is open by A3;

for X being Subset of T st X in F holds

X is dense by A3;

then A5: ( F is open & F is dense ) by A4;

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

assume A1: ( T is sober & T is locally-compact ) ; :: thesis: T is Baire

let F be Subset-Family of T; :: according to WAYBEL12:def 6 :: 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 )

A4: F is open by A3;

for X being Subset of T st X in F holds

X is dense by A3;

then A5: ( F is open & F is dense ) by A4;

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

per cases
( F <> {} or F = {} )
;

end;

suppose A6:
F <> {}
; :: thesis: I is dense

for Q being Subset of T st Q <> {} & Q is open holds

Intersect F meets Q

end;Intersect F meets Q

proof

hence
I is dense
by TOPS_1:45; :: thesis: verum
let Q be Subset of T; :: thesis: ( Q <> {} & Q is open implies Intersect F meets Q )

assume that

A7: Q <> {} and

A8: Q is open ; :: thesis: Intersect F meets Q

consider S being irreducible Subset of T such that

A9: for V being Subset of T st V in F holds

S /\ Q meets V by A1, A2, A5, A6, A7, A8, Th43;

consider p being Point of T such that

A10: p is_dense_point_of S and

for q being Point of T st q is_dense_point_of S holds

p = q by A1;

S is closed by YELLOW_8:def 3;

then A11: S = Cl {p} by A10, YELLOW_8:16;

A12: for Y being set st Y in F holds

( p in Y & p in Q )

p in Y ;

then A16: p in Intersect F by SETFAM_1:43;

ex Y being object st Y in F by A6, XBOOLE_0:def 1;

then p in Q by A12;

then (Intersect F) /\ Q <> {} by A16, XBOOLE_0:def 4;

hence Intersect F meets Q ; :: thesis: verum

end;assume that

A7: Q <> {} and

A8: Q is open ; :: thesis: Intersect F meets Q

consider S being irreducible Subset of T such that

A9: for V being Subset of T st V in F holds

S /\ Q meets V by A1, A2, A5, A6, A7, A8, Th43;

consider p being Point of T such that

A10: p is_dense_point_of S and

for q being Point of T st q is_dense_point_of S holds

p = q by A1;

S is closed by YELLOW_8:def 3;

then A11: S = Cl {p} by A10, YELLOW_8:16;

A12: for Y being set st Y in F holds

( p in Y & p in Q )

proof

then
for Y being set st Y in F holds
let Y be set ; :: thesis: ( Y in F implies ( p in Y & p in Q ) )

assume A13: Y in F ; :: thesis: ( p in Y & p in Q )

then reconsider Y1 = Y as Subset of T ;

S /\ Q meets Y1 by A9, A13;

then A14: (S /\ Q) /\ Y1 <> {} ;

end;assume A13: Y in F ; :: thesis: ( p in Y & p in Q )

then reconsider Y1 = Y as Subset of T ;

S /\ Q meets Y1 by A9, A13;

then A14: (S /\ Q) /\ Y1 <> {} ;

now :: thesis: p in Q /\ Y1

hence
( p in Y & p in Q )
by XBOOLE_0:def 4; :: thesis: verumassume
not p in Q /\ Y1
; :: thesis: contradiction

then p in (Q /\ Y1) ` by XBOOLE_0:def 5;

then {p} c= (Q /\ Y1) ` by ZFMISC_1:31;

then A15: Cl {p} c= Cl ((Q /\ Y1) `) by PRE_TOPC:19;

Y1 is open by A3, A13;

then Q /\ Y1 is open by A8;

then (Q /\ Y1) ` is closed ;

then S c= (Q /\ Y1) ` by A11, A15, PRE_TOPC:22;

then S misses Q /\ Y1 by SUBSET_1:23;

then S /\ (Q /\ Y1) = {} ;

hence contradiction by A14, XBOOLE_1:16; :: thesis: verum

end;then p in (Q /\ Y1) ` by XBOOLE_0:def 5;

then {p} c= (Q /\ Y1) ` by ZFMISC_1:31;

then A15: Cl {p} c= Cl ((Q /\ Y1) `) by PRE_TOPC:19;

Y1 is open by A3, A13;

then Q /\ Y1 is open by A8;

then (Q /\ Y1) ` is closed ;

then S c= (Q /\ Y1) ` by A11, A15, PRE_TOPC:22;

then S misses Q /\ Y1 by SUBSET_1:23;

then S /\ (Q /\ Y1) = {} ;

hence contradiction by A14, XBOOLE_1:16; :: thesis: verum

p in Y ;

then A16: p in Intersect F by SETFAM_1:43;

ex Y being object st Y in F by A6, XBOOLE_0:def 1;

then p in Q by A12;

then (Intersect F) /\ Q <> {} by A16, XBOOLE_0:def 4;

hence Intersect F meets Q ; :: thesis: verum