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
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:
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 ;
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 ;
then A14: (S /\ Q) /\ Y1 <> {} ;
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 object st Y in F by ;
then p in Q by A12;
then (Intersect F) /\ Q <> {} by ;
hence Intersect F meets Q ; :: thesis: verum
end;
hence I is dense by TOPS_1:45; :: thesis: verum
end;
suppose F = {} ; :: thesis: I is dense
end;
end;