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

proof

let X be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not X in F or X is open )
assume X in F ; :: thesis: X is open
hence X is open by A3; :: thesis: verum

end;

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, Def2;
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 = {} ) ;

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

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

proof

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, Th47;
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, YELLOW_8:def 5;
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

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 <> {} by XBOOLE_0:def 7;

now

assume 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) = {} by XBOOLE_0:def 7;
hence contradiction by A14, XBOOLE_1:16; :: thesis: verum

end;

hence ( p in Y & p in Q ) by XBOOLE_0:def 4; :: thesis: verum

end;

then for Y being set st Y in F holds
p in Y ;
then A16: p in Intersect F by SETFAM_1:43;
ex Y being set 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 by XBOOLE_0:def 7; :: thesis: verum

end;

hence I is dense by TOPS_1:45; :: thesis: verum

end;

suppose F = {} ; :: thesis: I is dense

then Intersect F = [#] T by SETFAM_1:def 9;
hence I is dense ; :: thesis: verum

end;

end;