let X be non empty Hausdorff TopSpace; :: thesis: for E being non empty Subset of X st X | E is dense & X | E is locally-compact holds
X | E is open

let E be non empty Subset of X; :: thesis: ( X | E is dense & X | E is locally-compact implies X | E is open )
assume A1: ( X | E is dense & X | E is locally-compact ) ; :: thesis: X | E is open
A2: [#] (X | E) = E by PRE_TOPC:8;
Int E = E
proof
thus Int E c= E by TOPS_1:16; :: according to XBOOLE_0:def 10 :: thesis: E c= Int E
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in E or a in Int E )
assume A3: a in E ; :: thesis: a in Int E
then reconsider x = a as Point of X ;
reconsider xx = x as Point of (X | E) by ;
set UE = { G where G is Subset of X : ( G is open & G c= E ) } ;
consider K being a_neighborhood of xx such that
A4: K is compact by A1;
reconsider KK = K as Subset of X by ;
A5: K c= [#] (X | E) ;
Int K in the topology of (X | E) by PRE_TOPC:def 2;
then consider G being Subset of X such that
A6: G in the topology of X and
A7: Int K = G /\ E by ;
A8: G is open by A6;
for P being Subset of (X | E) st P = KK holds
P is compact by A4;
then KK is compact by ;
then A9: Cl (G /\ E) c= KK by ;
E is dense by ;
then A10: Cl (G /\ E) = Cl G by ;
G c= Cl G by PRE_TOPC:18;
then G c= K by ;
then G c= E by ;
then A11: G in { G where G is Subset of X : ( G is open & G c= E ) } by A8;
A12: xx in Int K by CONNSP_2:def 1;
Int K c= G by ;
then a in union { G where G is Subset of X : ( G is open & G c= E ) } by ;
hence a in Int E by TEX_4:3; :: thesis: verum
end;
hence X | E is open by ; :: thesis: verum